This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem utop3cls

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)

Ref Expression
Hypothesis utoptop.1 
|- J = ( unifTop ` U )
Assertion 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

Step Hyp Ref Expression
1 utoptop.1 
 |-  J = ( unifTop ` U )
2 relxp 
 |-  Rel ( X X. X )
3 utoptop 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) e. Top )
4 1 3 eqeltrid 
 |-  ( U e. ( UnifOn ` X ) -> J e. Top )
5 txtop 
 |-  ( ( J e. Top /\ J e. Top ) -> ( J tX J ) e. Top )
6 4 4 5 syl2anc 
 |-  ( U e. ( UnifOn ` X ) -> ( J tX J ) e. Top )
7 6 ad3antrrr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) e. ( TopOn ` X ) )
10 1 9 eqeltrid 
 |-  ( U e. ( UnifOn ` X ) -> J e. ( TopOn ` X ) )
11 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
12 10 11 syl 
 |-  ( U e. ( UnifOn ` X ) -> X = U. J )
13 12 sqxpeqd 
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) = ( U. J X. U. J ) )
14 eqid 
 |-  U. J = U. J
15 14 14 txuni 
 |-  ( ( J e. Top /\ J e. Top ) -> ( U. J X. U. J ) = U. ( J tX J ) )
16 4 4 15 syl2anc 
 |-  ( U e. ( UnifOn ` X ) -> ( U. J X. U. J ) = U. ( J tX J ) )
17 13 16 eqtrd 
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) = U. ( J tX J ) )
18 17 ad3antrrr 
 |-  ( ( ( ( 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 ) )
19 8 18 sseqtrd 
 |-  ( ( ( ( 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 
 |-  U. ( J tX J ) = U. ( J tX J )
21 20 clsss3 
 |-  ( ( ( J tX J ) e. Top /\ M C_ U. ( J tX J ) ) -> ( ( cls ` ( J tX J ) ) ` M ) C_ U. ( J tX J ) )
22 7 19 21 syl2anc 
 |-  ( ( ( ( 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 ) )
23 22 18 sseqtrrd 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 ) )
25 23 24 sseldd 
 |-  ( ( ( ( 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 
 |-  ( ( Rel ( X X. X ) /\ z e. ( X X. X ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
27 2 25 26 sylancr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( 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 )
30 29 3anassrs 
 |-  ( ( ( ( ( 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 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> Rel V )
32 28 30 31 syl2anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( r e. ( ( ( V " { ( 1st ` z ) } ) X. ( V " { ( 2nd ` z ) } ) ) i^i M ) <-> ( r e. ( ( V " { ( 1st ` z ) } ) X. ( V " { ( 2nd ` z ) } ) ) /\ r e. M ) )
35 33 34 sylib 
 |-  ( ( ( ( ( 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 ) )
36 35 simpld 
 |-  ( ( ( ( ( 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 
 |-  ( r e. ( ( V " { ( 1st ` z ) } ) X. ( V " { ( 2nd ` z ) } ) ) -> ( 1st ` r ) e. ( V " { ( 1st ` z ) } ) )
38 36 37 syl 
 |-  ( ( ( ( ( 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 
 |-  ( Rel V -> ( ( 1st ` r ) e. ( V " { ( 1st ` z ) } ) <-> ( 1st ` z ) V ( 1st ` r ) ) )
40 39 biimpa 
 |-  ( ( Rel V /\ ( 1st ` r ) e. ( V " { ( 1st ` z ) } ) ) -> ( 1st ` z ) V ( 1st ` r ) )
41 32 38 40 syl2anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( X X. X ) C_ ( _V X. _V )
44 42 43 sstrdi 
 |-  ( ( ( ( ( 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 
 |-  ( Rel M <-> M C_ ( _V X. _V ) )
46 44 45 sylibr 
 |-  ( ( ( ( ( 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 )
47 35 simprd 
 |-  ( ( ( ( ( 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 
 |-  ( ( Rel M /\ r e. M ) -> ( 1st ` r ) M ( 2nd ` r ) )
49 46 47 48 syl2anc 
 |-  ( ( ( ( ( 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 
 |-  ( r e. ( ( V " { ( 1st ` z ) } ) X. ( V " { ( 2nd ` z ) } ) ) -> ( 2nd ` r ) e. ( V " { ( 2nd ` z ) } ) )
51 36 50 syl 
 |-  ( ( ( ( ( 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 
 |-  ( Rel V -> ( ( 2nd ` r ) e. ( V " { ( 2nd ` z ) } ) <-> ( 2nd ` z ) V ( 2nd ` r ) ) )
53 52 biimpa 
 |-  ( ( Rel V /\ ( 2nd ` r ) e. ( V " { ( 2nd ` z ) } ) ) -> ( 2nd ` z ) V ( 2nd ` r ) )
54 32 51 53 syl2anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( 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 )
56 55 3anassrs 
 |-  ( ( ( ( ( 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 breq 
 |-  ( `' V = V -> ( ( 2nd ` r ) `' V ( 2nd ` z ) <-> ( 2nd ` r ) V ( 2nd ` z ) ) )
58 fvex 
 |-  ( 2nd ` r ) e. _V
59 fvex 
 |-  ( 2nd ` z ) e. _V
60 58 59 brcnv 
 |-  ( ( 2nd ` r ) `' V ( 2nd ` z ) <-> ( 2nd ` z ) V ( 2nd ` r ) )
61 57 60 bitr3di 
 |-  ( `' V = V -> ( ( 2nd ` r ) V ( 2nd ` z ) <-> ( 2nd ` z ) V ( 2nd ` r ) ) )
62 56 61 syl 
 |-  ( ( ( ( ( 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 ) ) )
63 54 62 mpbird 
 |-  ( ( ( ( ( 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 
 |-  ( 1st ` z ) e. _V
65 fvex 
 |-  ( 1st ` r ) e. _V
66 brcogw 
 |-  ( ( ( ( 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 ) )
67 66 ex 
 |-  ( ( ( 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 ) ) )
68 64 58 65 67 mp3an 
 |-  ( ( ( 1st ` z ) V ( 1st ` r ) /\ ( 1st ` r ) M ( 2nd ` r ) ) -> ( 1st ` z ) ( M o. V ) ( 2nd ` r ) )
69 brcogw 
 |-  ( ( ( ( 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 ) )
70 69 ex 
 |-  ( ( ( 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 ) ) )
71 64 59 58 70 mp3an 
 |-  ( ( ( 1st ` z ) ( M o. V ) ( 2nd ` r ) /\ ( 2nd ` r ) V ( 2nd ` z ) ) -> ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) )
72 68 71 sylan 
 |-  ( ( ( ( 1st ` z ) V ( 1st ` r ) /\ ( 1st ` r ) M ( 2nd ` r ) ) /\ ( 2nd ` r ) V ( 2nd ` z ) ) -> ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) )
73 41 49 63 72 syl21anc 
 |-  ( ( ( ( ( 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 ) )
74 73 ralrimiva 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ M C_ ( X X. X ) ) /\ ( V e. U /\ `' V = V ) ) /\ z e. ( ( cls ` ( J tX J ) ) ` M ) ) -> V e. U )
77 4 3ad2ant1 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ z e. ( X X. X ) ) -> J e. Top )
78 xp1st 
 |-  ( z e. ( X X. X ) -> ( 1st ` z ) e. X )
79 1 utopsnnei 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ ( 1st ` z ) e. X ) -> ( V " { ( 1st ` z ) } ) e. ( ( nei ` J ) ` { ( 1st ` z ) } ) )
80 78 79 syl3an3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ z e. ( X X. X ) ) -> ( V " { ( 1st ` z ) } ) e. ( ( nei ` J ) ` { ( 1st ` z ) } ) )
81 xp2nd 
 |-  ( z e. ( X X. X ) -> ( 2nd ` z ) e. X )
82 1 utopsnnei 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ ( 2nd ` z ) e. X ) -> ( V " { ( 2nd ` z ) } ) e. ( ( nei ` J ) ` { ( 2nd ` z ) } ) )
83 81 82 syl3an3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ z e. ( X X. X ) ) -> ( V " { ( 2nd ` z ) } ) e. ( ( nei ` J ) ` { ( 2nd ` z ) } ) )
84 14 14 neitx 
 |-  ( ( ( 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 ) } ) ) )
85 77 77 80 83 84 syl22anc 
 |-  ( ( 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 
 |-  ( z e. ( X X. X ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
87 86 sneqd 
 |-  ( z e. ( X X. X ) -> { z } = { <. ( 1st ` z ) , ( 2nd ` z ) >. } )
88 64 59 xpsn 
 |-  ( { ( 1st ` z ) } X. { ( 2nd ` z ) } ) = { <. ( 1st ` z ) , ( 2nd ` z ) >. }
89 87 88 eqtr4di 
 |-  ( z e. ( X X. X ) -> { z } = ( { ( 1st ` z ) } X. { ( 2nd ` z ) } ) )
90 89 fveq2d 
 |-  ( z e. ( X X. X ) -> ( ( nei ` ( J tX J ) ) ` { z } ) = ( ( nei ` ( J tX J ) ) ` ( { ( 1st ` z ) } X. { ( 2nd ` z ) } ) ) )
91 90 3ad2ant3 
 |-  ( ( 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 ) } ) ) )
92 85 91 eleqtrrd 
 |-  ( ( 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 } ) )
93 75 76 25 92 syl3anc 
 |-  ( ( ( ( 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 } ) )
94 20 neindisj 
 |-  ( ( ( ( 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 ) =/= (/) )
95 7 19 24 93 94 syl22anc 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 ) ) )
97 95 96 syl 
 |-  ( ( ( ( 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 ) ) )
98 74 97 mpbird 
 |-  ( ( ( ( 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 
 |-  ( ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) <-> <. ( 1st ` z ) , ( 2nd ` z ) >. e. ( V o. ( M o. V ) ) )
100 98 99 sylib 
 |-  ( ( ( ( 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 ) ) )
101 27 100 eqeltrd 
 |-  ( ( ( ( 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 ) ) )
102 101 ex 
 |-  ( ( ( 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 ) ) ) )
103 102 ssrdv 
 |-  ( ( ( 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 ) ) )