Metamath Proof Explorer

Theorem utop2nei

Description: For any symmetrical entourage V and any relation M , build a neighborhood of M . First part of proposition 2 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018)

Ref Expression
Hypothesis utoptop.1 
|- J = ( unifTop ` U )
Assertion utop2nei 
|- ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) )

Proof

Step Hyp Ref Expression
1 utoptop.1 
 |-  J = ( unifTop ` U )
2 utoptop 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) e. Top )
3 1 2 eqeltrid 
 |-  ( U e. ( UnifOn ` X ) -> J e. Top )
4 txtop 
 |-  ( ( J e. Top /\ J e. Top ) -> ( J tX J ) e. Top )
5 3 3 4 syl2anc 
 |-  ( U e. ( UnifOn ` X ) -> ( J tX J ) e. Top )
6 5 3ad2ant1 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( J tX J ) e. Top )
7 6 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M = (/) ) -> ( J tX J ) e. Top )
8 0nei 
 |-  ( ( J tX J ) e. Top -> (/) e. ( ( nei ` ( J tX J ) ) ` (/) ) )
9 7 8 syl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M = (/) ) -> (/) e. ( ( nei ` ( J tX J ) ) ` (/) ) )
10 coeq1 
 |-  ( M = (/) -> ( M o. V ) = ( (/) o. V ) )
11 co01 
 |-  ( (/) o. V ) = (/)
12 10 11 eqtrdi 
 |-  ( M = (/) -> ( M o. V ) = (/) )
13 12 coeq2d 
 |-  ( M = (/) -> ( V o. ( M o. V ) ) = ( V o. (/) ) )
14 co02 
 |-  ( V o. (/) ) = (/)
15 13 14 eqtrdi 
 |-  ( M = (/) -> ( V o. ( M o. V ) ) = (/) )
16 15 adantl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M = (/) ) -> ( V o. ( M o. V ) ) = (/) )
17 simpr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M = (/) ) -> M = (/) )
18 17 fveq2d 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M = (/) ) -> ( ( nei ` ( J tX J ) ) ` M ) = ( ( nei ` ( J tX J ) ) ` (/) ) )
19 9 16 18 3eltr4d 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M = (/) ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) )
20 6 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( J tX J ) e. Top )
21 simpl1 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> U e. ( UnifOn ` X ) )
22 21 3 syl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> J e. Top )
23 simpl2l 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> V e. U )
24 simp3 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> M C_ ( X X. X ) )
25 24 sselda 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> r e. ( X X. X ) )
26 xp1st 
 |-  ( r e. ( X X. X ) -> ( 1st ` r ) e. X )
27 25 26 syl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( 1st ` r ) e. X )
28 1 utopsnnei 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ ( 1st ` r ) e. X ) -> ( V " { ( 1st ` r ) } ) e. ( ( nei ` J ) ` { ( 1st ` r ) } ) )
29 21 23 27 28 syl3anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( V " { ( 1st ` r ) } ) e. ( ( nei ` J ) ` { ( 1st ` r ) } ) )
30 xp2nd 
 |-  ( r e. ( X X. X ) -> ( 2nd ` r ) e. X )
31 25 30 syl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( 2nd ` r ) e. X )
32 1 utopsnnei 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ ( 2nd ` r ) e. X ) -> ( V " { ( 2nd ` r ) } ) e. ( ( nei ` J ) ` { ( 2nd ` r ) } ) )
33 21 23 31 32 syl3anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( V " { ( 2nd ` r ) } ) e. ( ( nei ` J ) ` { ( 2nd ` r ) } ) )
34 eqid 
 |-  U. J = U. J
35 34 34 neitx 
 |-  ( ( ( J e. Top /\ J e. Top ) /\ ( ( V " { ( 1st ` r ) } ) e. ( ( nei ` J ) ` { ( 1st ` r ) } ) /\ ( V " { ( 2nd ` r ) } ) e. ( ( nei ` J ) ` { ( 2nd ` r ) } ) ) ) -> ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) e. ( ( nei ` ( J tX J ) ) ` ( { ( 1st ` r ) } X. { ( 2nd ` r ) } ) ) )
36 22 22 29 33 35 syl22anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) e. ( ( nei ` ( J tX J ) ) ` ( { ( 1st ` r ) } X. { ( 2nd ` r ) } ) ) )
37 fvex 
 |-  ( 1st ` r ) e. _V
38 fvex 
 |-  ( 2nd ` r ) e. _V
39 37 38 xpsn 
 |-  ( { ( 1st ` r ) } X. { ( 2nd ` r ) } ) = { <. ( 1st ` r ) , ( 2nd ` r ) >. }
40 39 fveq2i 
 |-  ( ( nei ` ( J tX J ) ) ` ( { ( 1st ` r ) } X. { ( 2nd ` r ) } ) ) = ( ( nei ` ( J tX J ) ) ` { <. ( 1st ` r ) , ( 2nd ` r ) >. } )
41 36 40 eleqtrdi 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) e. ( ( nei ` ( J tX J ) ) ` { <. ( 1st ` r ) , ( 2nd ` r ) >. } ) )
42 24 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> M C_ ( X X. X ) )
43 xpss 
 |-  ( X X. X ) C_ ( _V X. _V )
44 sstr 
 |-  ( ( M C_ ( X X. X ) /\ ( X X. X ) C_ ( _V X. _V ) ) -> M C_ ( _V X. _V ) )
45 43 44 mpan2 
 |-  ( M C_ ( X X. X ) -> M C_ ( _V X. _V ) )
46 df-rel 
 |-  ( Rel M <-> M C_ ( _V X. _V ) )
47 45 46 sylibr 
 |-  ( M C_ ( X X. X ) -> Rel M )
48 42 47 syl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> Rel M )
49 1st2nd 
 |-  ( ( Rel M /\ r e. M ) -> r = <. ( 1st ` r ) , ( 2nd ` r ) >. )
50 48 49 sylancom 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> r = <. ( 1st ` r ) , ( 2nd ` r ) >. )
51 50 sneqd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> { r } = { <. ( 1st ` r ) , ( 2nd ` r ) >. } )
52 51 fveq2d 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( ( nei ` ( J tX J ) ) ` { r } ) = ( ( nei ` ( J tX J ) ) ` { <. ( 1st ` r ) , ( 2nd ` r ) >. } ) )
53 41 52 eleqtrrd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) )
54 relxp 
 |-  Rel ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) )
55 54 a1i 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> Rel ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) )
56 1st2nd 
 |-  ( ( Rel ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
57 55 56 sylancom 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
58 simpll2 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( V e. U /\ `' V = V ) )
59 58 simprd 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> `' V = V )
60 simpll1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> U e. ( UnifOn ` X ) )
61 58 simpld 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> V e. U )
62 ustrel 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> Rel V )
63 60 61 62 syl2anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> Rel V )
64 xp1st 
 |-  ( z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) -> ( 1st ` z ) e. ( V " { ( 1st ` r ) } ) )
65 64 adantl 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( 1st ` z ) e. ( V " { ( 1st ` r ) } ) )
66 elrelimasn 
 |-  ( Rel V -> ( ( 1st ` z ) e. ( V " { ( 1st ` r ) } ) <-> ( 1st ` r ) V ( 1st ` z ) ) )
67 66 biimpa 
 |-  ( ( Rel V /\ ( 1st ` z ) e. ( V " { ( 1st ` r ) } ) ) -> ( 1st ` r ) V ( 1st ` z ) )
68 63 65 67 syl2anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( 1st ` r ) V ( 1st ` z ) )
69 fvex 
 |-  ( 1st ` z ) e. _V
70 37 69 brcnv 
 |-  ( ( 1st ` r ) `' V ( 1st ` z ) <-> ( 1st ` z ) V ( 1st ` r ) )
71 breq 
 |-  ( `' V = V -> ( ( 1st ` r ) `' V ( 1st ` z ) <-> ( 1st ` r ) V ( 1st ` z ) ) )
72 70 71 bitr3id 
 |-  ( `' V = V -> ( ( 1st ` z ) V ( 1st ` r ) <-> ( 1st ` r ) V ( 1st ` z ) ) )
73 72 biimpar 
 |-  ( ( `' V = V /\ ( 1st ` r ) V ( 1st ` z ) ) -> ( 1st ` z ) V ( 1st ` r ) )
74 59 68 73 syl2anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( 1st ` z ) V ( 1st ` r ) )
75 simpll3 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> M C_ ( X X. X ) )
76 simplr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> r e. M )
77 1st2ndbr 
 |-  ( ( Rel M /\ r e. M ) -> ( 1st ` r ) M ( 2nd ` r ) )
78 47 77 sylan 
 |-  ( ( M C_ ( X X. X ) /\ r e. M ) -> ( 1st ` r ) M ( 2nd ` r ) )
79 75 76 78 syl2anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( 1st ` r ) M ( 2nd ` r ) )
80 xp2nd 
 |-  ( z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) -> ( 2nd ` z ) e. ( V " { ( 2nd ` r ) } ) )
81 80 adantl 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( 2nd ` z ) e. ( V " { ( 2nd ` r ) } ) )
82 elrelimasn 
 |-  ( Rel V -> ( ( 2nd ` z ) e. ( V " { ( 2nd ` r ) } ) <-> ( 2nd ` r ) V ( 2nd ` z ) ) )
83 82 biimpa 
 |-  ( ( Rel V /\ ( 2nd ` z ) e. ( V " { ( 2nd ` r ) } ) ) -> ( 2nd ` r ) V ( 2nd ` z ) )
84 63 81 83 syl2anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( 2nd ` r ) V ( 2nd ` z ) )
85 69 38 37 3pm3.2i 
 |-  ( ( 1st ` z ) e. _V /\ ( 2nd ` r ) e. _V /\ ( 1st ` r ) e. _V )
86 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 ) )
87 85 86 mpan 
 |-  ( ( ( 1st ` z ) V ( 1st ` r ) /\ ( 1st ` r ) M ( 2nd ` r ) ) -> ( 1st ` z ) ( M o. V ) ( 2nd ` r ) )
88 fvex 
 |-  ( 2nd ` z ) e. _V
89 69 88 38 3pm3.2i 
 |-  ( ( 1st ` z ) e. _V /\ ( 2nd ` z ) e. _V /\ ( 2nd ` r ) e. _V )
90 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 ) )
91 89 90 mpan 
 |-  ( ( ( 1st ` z ) ( M o. V ) ( 2nd ` r ) /\ ( 2nd ` r ) V ( 2nd ` z ) ) -> ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) )
92 87 91 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 ) )
93 74 79 84 92 syl21anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) )
94 df-br 
 |-  ( ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) <-> <. ( 1st ` z ) , ( 2nd ` z ) >. e. ( V o. ( M o. V ) ) )
95 93 94 sylib 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> <. ( 1st ` z ) , ( 2nd ` z ) >. e. ( V o. ( M o. V ) ) )
96 57 95 eqeltrd 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) /\ z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) ) -> z e. ( V o. ( M o. V ) ) )
97 96 ex 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( z e. ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) -> z e. ( V o. ( M o. V ) ) ) )
98 97 ssrdv 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) C_ ( V o. ( M o. V ) ) )
99 simp1 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> U e. ( UnifOn ` X ) )
100 simp2l 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> V e. U )
101 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( X X. X ) )
102 99 100 101 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> V C_ ( X X. X ) )
103 coss1 
 |-  ( V C_ ( X X. X ) -> ( V o. ( M o. V ) ) C_ ( ( X X. X ) o. ( M o. V ) ) )
104 102 103 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( V o. ( M o. V ) ) C_ ( ( X X. X ) o. ( M o. V ) ) )
105 coss1 
 |-  ( M C_ ( X X. X ) -> ( M o. V ) C_ ( ( X X. X ) o. V ) )
106 24 105 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( M o. V ) C_ ( ( X X. X ) o. V ) )
107 coss2 
 |-  ( V C_ ( X X. X ) -> ( ( X X. X ) o. V ) C_ ( ( X X. X ) o. ( X X. X ) ) )
108 xpcoid 
 |-  ( ( X X. X ) o. ( X X. X ) ) = ( X X. X )
109 107 108 sseqtrdi 
 |-  ( V C_ ( X X. X ) -> ( ( X X. X ) o. V ) C_ ( X X. X ) )
110 102 109 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( ( X X. X ) o. V ) C_ ( X X. X ) )
111 106 110 sstrd 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( M o. V ) C_ ( X X. X ) )
112 coss2 
 |-  ( ( M o. V ) C_ ( X X. X ) -> ( ( X X. X ) o. ( M o. V ) ) C_ ( ( X X. X ) o. ( X X. X ) ) )
113 112 108 sseqtrdi 
 |-  ( ( M o. V ) C_ ( X X. X ) -> ( ( X X. X ) o. ( M o. V ) ) C_ ( X X. X ) )
114 111 113 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( ( X X. X ) o. ( M o. V ) ) C_ ( X X. X ) )
115 104 114 sstrd 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( V o. ( M o. V ) ) C_ ( X X. X ) )
116 utopbas 
 |-  ( U e. ( UnifOn ` X ) -> X = U. ( unifTop ` U ) )
117 1 unieqi 
 |-  U. J = U. ( unifTop ` U )
118 116 117 eqtr4di 
 |-  ( U e. ( UnifOn ` X ) -> X = U. J )
119 118 sqxpeqd 
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) = ( U. J X. U. J ) )
120 34 34 txuni 
 |-  ( ( J e. Top /\ J e. Top ) -> ( U. J X. U. J ) = U. ( J tX J ) )
121 3 3 120 syl2anc 
 |-  ( U e. ( UnifOn ` X ) -> ( U. J X. U. J ) = U. ( J tX J ) )
122 119 121 eqtrd 
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) = U. ( J tX J ) )
123 122 3ad2ant1 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( X X. X ) = U. ( J tX J ) )
124 115 123 sseqtrd 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( V o. ( M o. V ) ) C_ U. ( J tX J ) )
125 124 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( V o. ( M o. V ) ) C_ U. ( J tX J ) )
126 eqid 
 |-  U. ( J tX J ) = U. ( J tX J )
127 126 ssnei2 
 |-  ( ( ( ( J tX J ) e. Top /\ ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) ) /\ ( ( ( V " { ( 1st ` r ) } ) X. ( V " { ( 2nd ` r ) } ) ) C_ ( V o. ( M o. V ) ) /\ ( V o. ( M o. V ) ) C_ U. ( J tX J ) ) ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) )
128 20 53 98 125 127 syl22anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ r e. M ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) )
129 128 ralrimiva 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> A. r e. M ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) )
130 129 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M =/= (/) ) -> A. r e. M ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) )
131 6 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M =/= (/) ) -> ( J tX J ) e. Top )
132 24 123 sseqtrd 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> M C_ U. ( J tX J ) )
133 132 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M =/= (/) ) -> M C_ U. ( J tX J ) )
134 simpr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M =/= (/) ) -> M =/= (/) )
135 126 neips 
 |-  ( ( ( J tX J ) e. Top /\ M C_ U. ( J tX J ) /\ M =/= (/) ) -> ( ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) <-> A. r e. M ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) ) )
136 131 133 134 135 syl3anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M =/= (/) ) -> ( ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) <-> A. r e. M ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` { r } ) ) )
137 130 136 mpbird 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) /\ M =/= (/) ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) )
138 19 137 pm2.61dane 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) )