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 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 ) )
29 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 )
30 4 3ad2ant1 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ z e. ( X X. X ) ) -> J e. Top )
31 xp1st 
 |-  ( z e. ( X X. X ) -> ( 1st ` z ) e. X )
32 1 utopsnnei 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ ( 1st ` z ) e. X ) -> ( V " { ( 1st ` z ) } ) e. ( ( nei ` J ) ` { ( 1st ` z ) } ) )
33 31 32 syl3an3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ z e. ( X X. X ) ) -> ( V " { ( 1st ` z ) } ) e. ( ( nei ` J ) ` { ( 1st ` z ) } ) )
34 xp2nd 
 |-  ( z e. ( X X. X ) -> ( 2nd ` z ) e. X )
35 1 utopsnnei 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ ( 2nd ` z ) e. X ) -> ( V " { ( 2nd ` z ) } ) e. ( ( nei ` J ) ` { ( 2nd ` z ) } ) )
36 34 35 syl3an3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ z e. ( X X. X ) ) -> ( V " { ( 2nd ` z ) } ) e. ( ( nei ` J ) ` { ( 2nd ` z ) } ) )
37 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 ) } ) ) )
38 30 30 33 36 37 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 ) } ) ) )
39 1st2nd2 
 |-  ( z e. ( X X. X ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
40 39 sneqd 
 |-  ( z e. ( X X. X ) -> { z } = { <. ( 1st ` z ) , ( 2nd ` z ) >. } )
41 fvex 
 |-  ( 1st ` z ) e. _V
42 fvex 
 |-  ( 2nd ` z ) e. _V
43 41 42 xpsn 
 |-  ( { ( 1st ` z ) } X. { ( 2nd ` z ) } ) = { <. ( 1st ` z ) , ( 2nd ` z ) >. }
44 40 43 eqtr4di 
 |-  ( z e. ( X X. X ) -> { z } = ( { ( 1st ` z ) } X. { ( 2nd ` z ) } ) )
45 44 fveq2d 
 |-  ( z e. ( X X. X ) -> ( ( nei ` ( J tX J ) ) ` { z } ) = ( ( nei ` ( J tX J ) ) ` ( { ( 1st ` z ) } X. { ( 2nd ` z ) } ) ) )
46 45 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 ) } ) ) )
47 38 46 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 } ) )
48 28 29 25 47 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 } ) )
49 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 ) =/= (/) )
50 7 19 24 48 49 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 ) =/= (/) )
51 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 ) )
52 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 )
53 52 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 )
54 ustrel 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> Rel V )
55 51 53 54 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 )
56 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 ) )
57 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 ) )
58 56 57 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 ) )
59 58 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 ) } ) ) )
60 xp1st 
 |-  ( r e. ( ( V " { ( 1st ` z ) } ) X. ( V " { ( 2nd ` z ) } ) ) -> ( 1st ` r ) e. ( V " { ( 1st ` z ) } ) )
61 59 60 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 ) } ) )
62 elrelimasn 
 |-  ( Rel V -> ( ( 1st ` r ) e. ( V " { ( 1st ` z ) } ) <-> ( 1st ` z ) V ( 1st ` r ) ) )
63 62 biimpa 
 |-  ( ( Rel V /\ ( 1st ` r ) e. ( V " { ( 1st ` z ) } ) ) -> ( 1st ` z ) V ( 1st ` r ) )
64 55 61 63 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 ) )
65 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 ) )
66 xpss 
 |-  ( X X. X ) C_ ( _V X. _V )
67 65 66 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 ) )
68 df-rel 
 |-  ( Rel M <-> M C_ ( _V X. _V ) )
69 67 68 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 )
70 58 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 )
71 1st2ndbr 
 |-  ( ( Rel M /\ r e. M ) -> ( 1st ` r ) M ( 2nd ` r ) )
72 69 70 71 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 ) )
73 xp2nd 
 |-  ( r e. ( ( V " { ( 1st ` z ) } ) X. ( V " { ( 2nd ` z ) } ) ) -> ( 2nd ` r ) e. ( V " { ( 2nd ` z ) } ) )
74 59 73 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 ) } ) )
75 elrelimasn 
 |-  ( Rel V -> ( ( 2nd ` r ) e. ( V " { ( 2nd ` z ) } ) <-> ( 2nd ` z ) V ( 2nd ` r ) ) )
76 75 biimpa 
 |-  ( ( Rel V /\ ( 2nd ` r ) e. ( V " { ( 2nd ` z ) } ) ) -> ( 2nd ` z ) V ( 2nd ` r ) )
77 55 74 76 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 ) )
78 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 )
79 78 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 )
80 breq 
 |-  ( `' V = V -> ( ( 2nd ` r ) `' V ( 2nd ` z ) <-> ( 2nd ` r ) V ( 2nd ` z ) ) )
81 fvex 
 |-  ( 2nd ` r ) e. _V
82 81 42 brcnv 
 |-  ( ( 2nd ` r ) `' V ( 2nd ` z ) <-> ( 2nd ` z ) V ( 2nd ` r ) )
83 80 82 bitr3di 
 |-  ( `' V = V -> ( ( 2nd ` r ) V ( 2nd ` z ) <-> ( 2nd ` z ) V ( 2nd ` r ) ) )
84 79 83 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 ) ) )
85 77 84 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 ) )
86 fvex 
 |-  ( 1st ` r ) e. _V
87 41 86 81 brcoi 
 |-  ( ( ( 1st ` z ) V ( 1st ` r ) /\ ( 1st ` r ) M ( 2nd ` r ) ) -> ( 1st ` z ) ( M o. V ) ( 2nd ` r ) )
88 41 81 42 brcoi 
 |-  ( ( ( 1st ` z ) ( M o. V ) ( 2nd ` r ) /\ ( 2nd ` r ) V ( 2nd ` z ) ) -> ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) )
89 87 88 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 ) )
90 64 72 85 89 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 ) )
91 50 90 n0limd 
 |-  ( ( ( ( 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 ) )
92 df-br 
 |-  ( ( 1st ` z ) ( V o. ( M o. V ) ) ( 2nd ` z ) <-> <. ( 1st ` z ) , ( 2nd ` z ) >. e. ( V o. ( M o. V ) ) )
93 91 92 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 ) ) )
94 27 93 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 ) ) )
95 94 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 ) ) ) )
96 95 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 ) ) )