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 ) ) )