MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  utop3cls Structured version   Unicode version

Theorem utop3cls 18312
Description: Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Jan-2018.)
Hypothesis
Ref Expression
utoptop.1  |-  J  =  (unifTop `  U )
Assertion
Ref Expression
utop3cls  |-  ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X
) )  /\  ( V  e.  U  /\  `' V  =  V
) )  ->  (
( cls `  ( J  tX  J ) ) `
 M )  C_  ( V  o.  ( M  o.  V )
) )

Proof of Theorem utop3cls
Dummy variables  r 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 5012 . . . . 5  |-  Rel  ( X  X.  X )
2 utoptop.1 . . . . . . . . . . 11  |-  J  =  (unifTop `  U )
3 utoptop 18295 . . . . . . . . . . 11  |-  ( U  e.  (UnifOn `  X
)  ->  (unifTop `  U
)  e.  Top )
42, 3syl5eqel 2526 . . . . . . . . . 10  |-  ( U  e.  (UnifOn `  X
)  ->  J  e.  Top )
5 txtop 17632 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  J  e.  Top )  ->  ( J  tX  J
)  e.  Top )
64, 4, 5syl2anc 644 . . . . . . . . 9  |-  ( U  e.  (UnifOn `  X
)  ->  ( J  tX  J )  e.  Top )
76ad3antrrr 712 . . . . . . . 8  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( J  tX  J
)  e.  Top )
8 simpllr 737 . . . . . . . . 9  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  ->  M  C_  ( X  X.  X ) )
9 utoptopon 18297 . . . . . . . . . . . . . 14  |-  ( U  e.  (UnifOn `  X
)  ->  (unifTop `  U
)  e.  (TopOn `  X ) )
102, 9syl5eqel 2526 . . . . . . . . . . . . 13  |-  ( U  e.  (UnifOn `  X
)  ->  J  e.  (TopOn `  X ) )
11 toponuni 17023 . . . . . . . . . . . . 13  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
1210, 11syl 16 . . . . . . . . . . . 12  |-  ( U  e.  (UnifOn `  X
)  ->  X  =  U. J )
1312, 12xpeq12d 4932 . . . . . . . . . . 11  |-  ( U  e.  (UnifOn `  X
)  ->  ( X  X.  X )  =  ( U. J  X.  U. J ) )
14 eqid 2442 . . . . . . . . . . . . 13  |-  U. J  =  U. J
1514, 14txuni 17655 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  J  e.  Top )  ->  ( U. J  X.  U. J )  =  U. ( J  tX  J ) )
164, 4, 15syl2anc 644 . . . . . . . . . . 11  |-  ( U  e.  (UnifOn `  X
)  ->  ( U. J  X.  U. J )  =  U. ( J 
tX  J ) )
1713, 16eqtrd 2474 . . . . . . . . . 10  |-  ( U  e.  (UnifOn `  X
)  ->  ( X  X.  X )  =  U. ( J  tX  J ) )
1817ad3antrrr 712 . . . . . . . . 9  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( X  X.  X
)  =  U. ( J  tX  J ) )
198, 18sseqtrd 3370 . . . . . . . 8  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  ->  M  C_  U. ( J 
tX  J ) )
20 eqid 2442 . . . . . . . . 9  |-  U. ( J  tX  J )  = 
U. ( J  tX  J )
2120clsss3 17154 . . . . . . . 8  |-  ( ( ( J  tX  J
)  e.  Top  /\  M  C_  U. ( J 
tX  J ) )  ->  ( ( cls `  ( J  tX  J
) ) `  M
)  C_  U. ( J  tX  J ) )
227, 19, 21syl2anc 644 . . . . . . 7  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( ( cls `  ( J  tX  J ) ) `
 M )  C_  U. ( J  tX  J
) )
2322, 18sseqtr4d 3371 . . . . . 6  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( ( cls `  ( J  tX  J ) ) `
 M )  C_  ( X  X.  X
) )
24 simpr 449 . . . . . 6  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
z  e.  ( ( cls `  ( J 
tX  J ) ) `
 M ) )
2523, 24sseldd 3335 . . . . 5  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
z  e.  ( X  X.  X ) )
26 1st2nd 6422 . . . . 5  |-  ( ( Rel  ( X  X.  X )  /\  z  e.  ( X  X.  X
) )  ->  z  =  <. ( 1st `  z
) ,  ( 2nd `  z ) >. )
271, 25, 26sylancr 646 . . . 4  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
28 simp-4l 744 . . . . . . . . . 10  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  U  e.  (UnifOn `  X ) )
29 simpr1l 1015 . . . . . . . . . . 11  |-  ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X
) )  /\  (
( V  e.  U  /\  `' V  =  V
)  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `
 M )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) ) )  ->  V  e.  U )
30293anassrs 1176 . . . . . . . . . 10  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  V  e.  U
)
31 ustrel 18272 . . . . . . . . . 10  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U )  ->  Rel  V )
3228, 30, 31syl2anc 644 . . . . . . . . 9  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  Rel  V )
33 simpr 449 . . . . . . . . . . . 12  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  r  e.  ( ( ( V " { ( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )
34 elin 3516 . . . . . . . . . . . 12  |-  ( r  e.  ( ( ( V " { ( 1st `  z ) } )  X.  ( V " { ( 2nd `  z ) } ) )  i^i  M )  <-> 
( r  e.  ( ( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  /\  r  e.  M
) )
3533, 34sylib 190 . . . . . . . . . . 11  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( r  e.  ( ( V " { ( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  /\  r  e.  M
) )
3635simpld 447 . . . . . . . . . 10  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  r  e.  ( ( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) ) )
37 xp1st 6405 . . . . . . . . . 10  |-  ( r  e.  ( ( V
" { ( 1st `  z ) } )  X.  ( V " { ( 2nd `  z
) } ) )  ->  ( 1st `  r
)  e.  ( V
" { ( 1st `  z ) } ) )
3836, 37syl 16 . . . . . . . . 9  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( 1st `  r
)  e.  ( V
" { ( 1st `  z ) } ) )
39 elrelimasn 5257 . . . . . . . . . 10  |-  ( Rel 
V  ->  ( ( 1st `  r )  e.  ( V " {
( 1st `  z
) } )  <->  ( 1st `  z ) V ( 1st `  r ) ) )
4039biimpa 472 . . . . . . . . 9  |-  ( ( Rel  V  /\  ( 1st `  r )  e.  ( V " {
( 1st `  z
) } ) )  ->  ( 1st `  z
) V ( 1st `  r ) )
4132, 38, 40syl2anc 644 . . . . . . . 8  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( 1st `  z
) V ( 1st `  r ) )
42 simp-4r 745 . . . . . . . . . . 11  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  M  C_  ( X  X.  X ) )
43 xpss 5011 . . . . . . . . . . 11  |-  ( X  X.  X )  C_  ( _V  X.  _V )
4442, 43syl6ss 3346 . . . . . . . . . 10  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  M  C_  ( _V  X.  _V ) )
45 df-rel 4914 . . . . . . . . . 10  |-  ( Rel 
M  <->  M  C_  ( _V 
X.  _V ) )
4644, 45sylibr 205 . . . . . . . . 9  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  Rel  M )
4735simprd 451 . . . . . . . . 9  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  r  e.  M
)
48 1st2ndbr 6425 . . . . . . . . 9  |-  ( ( Rel  M  /\  r  e.  M )  ->  ( 1st `  r ) M ( 2nd `  r
) )
4946, 47, 48syl2anc 644 . . . . . . . 8  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( 1st `  r
) M ( 2nd `  r ) )
50 xp2nd 6406 . . . . . . . . . . 11  |-  ( r  e.  ( ( V
" { ( 1st `  z ) } )  X.  ( V " { ( 2nd `  z
) } ) )  ->  ( 2nd `  r
)  e.  ( V
" { ( 2nd `  z ) } ) )
5136, 50syl 16 . . . . . . . . . 10  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( 2nd `  r
)  e.  ( V
" { ( 2nd `  z ) } ) )
52 elrelimasn 5257 . . . . . . . . . . 11  |-  ( Rel 
V  ->  ( ( 2nd `  r )  e.  ( V " {
( 2nd `  z
) } )  <->  ( 2nd `  z ) V ( 2nd `  r ) ) )
5352biimpa 472 . . . . . . . . . 10  |-  ( ( Rel  V  /\  ( 2nd `  r )  e.  ( V " {
( 2nd `  z
) } ) )  ->  ( 2nd `  z
) V ( 2nd `  r ) )
5432, 51, 53syl2anc 644 . . . . . . . . 9  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( 2nd `  z
) V ( 2nd `  r ) )
55 simpr1r 1016 . . . . . . . . . . 11  |-  ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X
) )  /\  (
( V  e.  U  /\  `' V  =  V
)  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `
 M )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) ) )  ->  `' V  =  V )
56553anassrs 1176 . . . . . . . . . 10  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  `' V  =  V )
57 fvex 5771 . . . . . . . . . . . 12  |-  ( 2nd `  r )  e.  _V
58 fvex 5771 . . . . . . . . . . . 12  |-  ( 2nd `  z )  e.  _V
5957, 58brcnv 5084 . . . . . . . . . . 11  |-  ( ( 2nd `  r ) `' V ( 2nd `  z
)  <->  ( 2nd `  z
) V ( 2nd `  r ) )
60 breq 4239 . . . . . . . . . . 11  |-  ( `' V  =  V  -> 
( ( 2nd `  r
) `' V ( 2nd `  z )  <-> 
( 2nd `  r
) V ( 2nd `  z ) ) )
6159, 60syl5rbbr 253 . . . . . . . . . 10  |-  ( `' V  =  V  -> 
( ( 2nd `  r
) V ( 2nd `  z )  <->  ( 2nd `  z ) V ( 2nd `  r ) ) )
6256, 61syl 16 . . . . . . . . 9  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( ( 2nd `  r ) V ( 2nd `  z )  <-> 
( 2nd `  z
) V ( 2nd `  r ) ) )
6354, 62mpbird 225 . . . . . . . 8  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( 2nd `  r
) V ( 2nd `  z ) )
64 fvex 5771 . . . . . . . . . 10  |-  ( 1st `  z )  e.  _V
65 fvex 5771 . . . . . . . . . 10  |-  ( 1st `  r )  e.  _V
66 brcogw 5070 . . . . . . . . . . 11  |-  ( ( ( ( 1st `  z
)  e.  _V  /\  ( 2nd `  r )  e.  _V  /\  ( 1st `  r )  e. 
_V )  /\  (
( 1st `  z
) V ( 1st `  r )  /\  ( 1st `  r ) M ( 2nd `  r
) ) )  -> 
( 1st `  z
) ( M  o.  V ) ( 2nd `  r ) )
6766ex 425 . . . . . . . . . 10  |-  ( ( ( 1st `  z
)  e.  _V  /\  ( 2nd `  r )  e.  _V  /\  ( 1st `  r )  e. 
_V )  ->  (
( ( 1st `  z
) V ( 1st `  r )  /\  ( 1st `  r ) M ( 2nd `  r
) )  ->  ( 1st `  z ) ( M  o.  V ) ( 2nd `  r
) ) )
6864, 57, 65, 67mp3an 1280 . . . . . . . . 9  |-  ( ( ( 1st `  z
) V ( 1st `  r )  /\  ( 1st `  r ) M ( 2nd `  r
) )  ->  ( 1st `  z ) ( M  o.  V ) ( 2nd `  r
) )
69 brcogw 5070 . . . . . . . . . . 11  |-  ( ( ( ( 1st `  z
)  e.  _V  /\  ( 2nd `  z )  e.  _V  /\  ( 2nd `  r )  e. 
_V )  /\  (
( 1st `  z
) ( M  o.  V ) ( 2nd `  r )  /\  ( 2nd `  r ) V ( 2nd `  z
) ) )  -> 
( 1st `  z
) ( V  o.  ( M  o.  V
) ) ( 2nd `  z ) )
7069ex 425 . . . . . . . . . 10  |-  ( ( ( 1st `  z
)  e.  _V  /\  ( 2nd `  z )  e.  _V  /\  ( 2nd `  r )  e. 
_V )  ->  (
( ( 1st `  z
) ( M  o.  V ) ( 2nd `  r )  /\  ( 2nd `  r ) V ( 2nd `  z
) )  ->  ( 1st `  z ) ( V  o.  ( M  o.  V ) ) ( 2nd `  z
) ) )
7164, 58, 57, 70mp3an 1280 . . . . . . . . 9  |-  ( ( ( 1st `  z
) ( M  o.  V ) ( 2nd `  r )  /\  ( 2nd `  r ) V ( 2nd `  z
) )  ->  ( 1st `  z ) ( V  o.  ( M  o.  V ) ) ( 2nd `  z
) )
7268, 71sylan 459 . . . . . . . 8  |-  ( ( ( ( 1st `  z
) V ( 1st `  r )  /\  ( 1st `  r ) M ( 2nd `  r
) )  /\  ( 2nd `  r ) V ( 2nd `  z
) )  ->  ( 1st `  z ) ( V  o.  ( M  o.  V ) ) ( 2nd `  z
) )
7341, 49, 63, 72syl21anc 1184 . . . . . . 7  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  /\  r  e.  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) )  ->  ( 1st `  z
) ( V  o.  ( M  o.  V
) ) ( 2nd `  z ) )
7473ralrimiva 2795 . . . . . 6  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  ->  A. r  e.  (
( ( V " { ( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) ( 1st `  z ) ( V  o.  ( M  o.  V )
) ( 2nd `  z
) )
75 simplll 736 . . . . . . . . 9  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  ->  U  e.  (UnifOn `  X
) )
76 simplrl 738 . . . . . . . . 9  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  ->  V  e.  U )
7743ad2ant1 979 . . . . . . . . . . 11  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  z  e.  ( X  X.  X
) )  ->  J  e.  Top )
78 xp1st 6405 . . . . . . . . . . . 12  |-  ( z  e.  ( X  X.  X )  ->  ( 1st `  z )  e.  X )
792utopsnnei 18310 . . . . . . . . . . . 12  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  ( 1st `  z )  e.  X )  ->  ( V " { ( 1st `  z ) } )  e.  ( ( nei `  J ) `  {
( 1st `  z
) } ) )
8078, 79syl3an3 1220 . . . . . . . . . . 11  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  z  e.  ( X  X.  X
) )  ->  ( V " { ( 1st `  z ) } )  e.  ( ( nei `  J ) `  {
( 1st `  z
) } ) )
81 xp2nd 6406 . . . . . . . . . . . 12  |-  ( z  e.  ( X  X.  X )  ->  ( 2nd `  z )  e.  X )
822utopsnnei 18310 . . . . . . . . . . . 12  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  ( 2nd `  z )  e.  X )  ->  ( V " { ( 2nd `  z ) } )  e.  ( ( nei `  J ) `  {
( 2nd `  z
) } ) )
8381, 82syl3an3 1220 . . . . . . . . . . 11  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  z  e.  ( X  X.  X
) )  ->  ( V " { ( 2nd `  z ) } )  e.  ( ( nei `  J ) `  {
( 2nd `  z
) } ) )
8414, 14neitx 17670 . . . . . . . . . . 11  |-  ( ( ( J  e.  Top  /\  J  e.  Top )  /\  ( ( V " { ( 1st `  z
) } )  e.  ( ( nei `  J
) `  { ( 1st `  z ) } )  /\  ( V
" { ( 2nd `  z ) } )  e.  ( ( nei `  J ) `  {
( 2nd `  z
) } ) ) )  ->  ( ( V " { ( 1st `  z ) } )  X.  ( V " { ( 2nd `  z
) } ) )  e.  ( ( nei `  ( J  tX  J
) ) `  ( { ( 1st `  z
) }  X.  {
( 2nd `  z
) } ) ) )
8577, 77, 80, 83, 84syl22anc 1186 . . . . . . . . . 10  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  z  e.  ( X  X.  X
) )  ->  (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  e.  ( ( nei `  ( J  tX  J
) ) `  ( { ( 1st `  z
) }  X.  {
( 2nd `  z
) } ) ) )
86 1st2nd2 6415 . . . . . . . . . . . . . 14  |-  ( z  e.  ( X  X.  X )  ->  z  =  <. ( 1st `  z
) ,  ( 2nd `  z ) >. )
8786sneqd 3851 . . . . . . . . . . . . 13  |-  ( z  e.  ( X  X.  X )  ->  { z }  =  { <. ( 1st `  z ) ,  ( 2nd `  z
) >. } )
8864, 58xpsn 5939 . . . . . . . . . . . . 13  |-  ( { ( 1st `  z
) }  X.  {
( 2nd `  z
) } )  =  { <. ( 1st `  z
) ,  ( 2nd `  z ) >. }
8987, 88syl6eqr 2492 . . . . . . . . . . . 12  |-  ( z  e.  ( X  X.  X )  ->  { z }  =  ( { ( 1st `  z
) }  X.  {
( 2nd `  z
) } ) )
9089fveq2d 5761 . . . . . . . . . . 11  |-  ( z  e.  ( X  X.  X )  ->  (
( nei `  ( J  tX  J ) ) `
 { z } )  =  ( ( nei `  ( J 
tX  J ) ) `
 ( { ( 1st `  z ) }  X.  { ( 2nd `  z ) } ) ) )
91903ad2ant3 981 . . . . . . . . . 10  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  z  e.  ( X  X.  X
) )  ->  (
( nei `  ( J  tX  J ) ) `
 { z } )  =  ( ( nei `  ( J 
tX  J ) ) `
 ( { ( 1st `  z ) }  X.  { ( 2nd `  z ) } ) ) )
9285, 91eleqtrrd 2519 . . . . . . . . 9  |-  ( ( U  e.  (UnifOn `  X )  /\  V  e.  U  /\  z  e.  ( X  X.  X
) )  ->  (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  e.  ( ( nei `  ( J  tX  J
) ) `  {
z } ) )
9375, 76, 25, 92syl3anc 1185 . . . . . . . 8  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( ( V " { ( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  e.  ( ( nei `  ( J  tX  J
) ) `  {
z } ) )
9420neindisj 17212 . . . . . . . 8  |-  ( ( ( ( J  tX  J )  e.  Top  /\  M  C_  U. ( J  tX  J ) )  /\  ( z  e.  ( ( cls `  ( J  tX  J ) ) `
 M )  /\  ( ( V " { ( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  e.  ( ( nei `  ( J  tX  J
) ) `  {
z } ) ) )  ->  ( (
( V " {
( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M )  =/=  (/) )
957, 19, 24, 93, 94syl22anc 1186 . . . . . . 7  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( ( ( V
" { ( 1st `  z ) } )  X.  ( V " { ( 2nd `  z
) } ) )  i^i  M )  =/=  (/) )
96 r19.3rzv 3745 . . . . . . 7  |-  ( ( ( ( V " { ( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M )  =/=  (/)  ->  ( ( 1st `  z ) ( V  o.  ( M  o.  V ) ) ( 2nd `  z )  <->  A. r  e.  (
( ( V " { ( 1st `  z
) } )  X.  ( V " {
( 2nd `  z
) } ) )  i^i  M ) ( 1st `  z ) ( V  o.  ( M  o.  V )
) ( 2nd `  z
) ) )
9795, 96syl 16 . . . . . 6  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( ( 1st `  z
) ( V  o.  ( M  o.  V
) ) ( 2nd `  z )  <->  A. r  e.  ( ( ( V
" { ( 1st `  z ) } )  X.  ( V " { ( 2nd `  z
) } ) )  i^i  M ) ( 1st `  z ) ( V  o.  ( M  o.  V )
) ( 2nd `  z
) ) )
9874, 97mpbird 225 . . . . 5  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
( 1st `  z
) ( V  o.  ( M  o.  V
) ) ( 2nd `  z ) )
99 df-br 4238 . . . . 5  |-  ( ( 1st `  z ) ( V  o.  ( M  o.  V )
) ( 2nd `  z
)  <->  <. ( 1st `  z
) ,  ( 2nd `  z ) >.  e.  ( V  o.  ( M  o.  V ) ) )
10098, 99sylib 190 . . . 4  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  ->  <. ( 1st `  z
) ,  ( 2nd `  z ) >.  e.  ( V  o.  ( M  o.  V ) ) )
10127, 100eqeltrd 2516 . . 3  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X ) )  /\  ( V  e.  U  /\  `' V  =  V ) )  /\  z  e.  ( ( cls `  ( J  tX  J ) ) `  M ) )  -> 
z  e.  ( V  o.  ( M  o.  V ) ) )
102101ex 425 . 2  |-  ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X
) )  /\  ( V  e.  U  /\  `' V  =  V
) )  ->  (
z  e.  ( ( cls `  ( J 
tX  J ) ) `
 M )  -> 
z  e.  ( V  o.  ( M  o.  V ) ) ) )
103102ssrdv 3340 1  |-  ( ( ( U  e.  (UnifOn `  X )  /\  M  C_  ( X  X.  X
) )  /\  ( V  e.  U  /\  `' V  =  V
) )  ->  (
( cls `  ( J  tX  J ) ) `
 M )  C_  ( V  o.  ( M  o.  V )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1727    =/= wne 2605   A.wral 2711   _Vcvv 2962    i^i cin 3305    C_ wss 3306   (/)c0 3613   {csn 3838   <.cop 3841   U.cuni 4039   class class class wbr 4237    X. cxp 4905   `'ccnv 4906   "cima 4910    o. ccom 4911   Rel wrel 4912   ` cfv 5483  (class class class)co 6110   1stc1st 6376   2ndc2nd 6377   Topctop 16989  TopOnctopon 16990   clsccl 17113   neicnei 17192    tX ctx 17623  UnifOncust 18260  unifTopcutop 18291
This theorem is referenced by:  utopreg  18313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-rep 4345  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-reu 2718  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-int 4075  df-iun 4119  df-iin 4120  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-1st 6378  df-2nd 6379  df-recs 6662  df-rdg 6697  df-1o 6753  df-oadd 6757  df-er 6934  df-en 7139  df-fin 7142  df-fi 7445  df-topgen 13698  df-top 16994  df-bases 16996  df-topon 16997  df-cld 17114  df-ntr 17115  df-cls 17116  df-nei 17193  df-tx 17625  df-ust 18261  df-utop 18292
  Copyright terms: Public domain W3C validator