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 𝐽 = ( unifTop ‘ 𝑈 )
Assertion utop3cls ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝑉 ∘ ( 𝑀𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 utoptop.1 𝐽 = ( unifTop ‘ 𝑈 )
2 relxp Rel ( 𝑋 × 𝑋 )
3 utoptop ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top )
4 1 3 eqeltrid ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 ∈ Top )
5 txtop ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐽 ×t 𝐽 ) ∈ Top )
6 4 4 5 syl2anc ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐽 ×t 𝐽 ) ∈ Top )
7 6 ad3antrrr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( 𝐽 ×t 𝐽 ) ∈ Top )
8 simpllr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑀 ⊆ ( 𝑋 × 𝑋 ) )
9 utoptopon ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ ( TopOn ‘ 𝑋 ) )
10 1 9 eqeltrid ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
12 10 11 syl ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
13 12 sqxpeqd ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ( 𝐽 × 𝐽 ) )
14 eqid 𝐽 = 𝐽
15 14 14 txuni ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐽 × 𝐽 ) = ( 𝐽 ×t 𝐽 ) )
16 4 4 15 syl2anc ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐽 × 𝐽 ) = ( 𝐽 ×t 𝐽 ) )
17 13 16 eqtrd ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ( 𝐽 ×t 𝐽 ) )
18 17 ad3antrrr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( 𝑋 × 𝑋 ) = ( 𝐽 ×t 𝐽 ) )
19 8 18 sseqtrd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑀 ( 𝐽 ×t 𝐽 ) )
20 eqid ( 𝐽 ×t 𝐽 ) = ( 𝐽 ×t 𝐽 )
21 20 clsss3 ( ( ( 𝐽 ×t 𝐽 ) ∈ Top ∧ 𝑀 ( 𝐽 ×t 𝐽 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝐽 ×t 𝐽 ) )
22 7 19 21 syl2anc ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝐽 ×t 𝐽 ) )
23 22 18 sseqtrrd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝑋 × 𝑋 ) )
24 simpr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) )
25 23 24 sseldd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 ∈ ( 𝑋 × 𝑋 ) )
26 1st2nd ( ( Rel ( 𝑋 × 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → 𝑧 = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
27 2 25 26 sylancr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
28 simp-4l ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
29 simpr1l ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑉𝑈 𝑉 = 𝑉 ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) ) → 𝑉𝑈 )
30 29 3anassrs ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑉𝑈 )
31 ustrel ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → Rel 𝑉 )
32 28 30 31 syl2anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → Rel 𝑉 )
33 simpr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) )
34 elin ( 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ↔ ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∧ 𝑟𝑀 ) )
35 33 34 sylib ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∧ 𝑟𝑀 ) )
36 35 simpld ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑟 ∈ ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) )
37 xp1st ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) → ( 1st𝑟 ) ∈ ( 𝑉 “ { ( 1st𝑧 ) } ) )
38 36 37 syl ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st𝑟 ) ∈ ( 𝑉 “ { ( 1st𝑧 ) } ) )
39 elrelimasn ( Rel 𝑉 → ( ( 1st𝑟 ) ∈ ( 𝑉 “ { ( 1st𝑧 ) } ) ↔ ( 1st𝑧 ) 𝑉 ( 1st𝑟 ) ) )
40 39 biimpa ( ( Rel 𝑉 ∧ ( 1st𝑟 ) ∈ ( 𝑉 “ { ( 1st𝑧 ) } ) ) → ( 1st𝑧 ) 𝑉 ( 1st𝑟 ) )
41 32 38 40 syl2anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st𝑧 ) 𝑉 ( 1st𝑟 ) )
42 simp-4r ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑀 ⊆ ( 𝑋 × 𝑋 ) )
43 xpss ( 𝑋 × 𝑋 ) ⊆ ( V × V )
44 42 43 sstrdi ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑀 ⊆ ( V × V ) )
45 df-rel ( Rel 𝑀𝑀 ⊆ ( V × V ) )
46 44 45 sylibr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → Rel 𝑀 )
47 35 simprd ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑟𝑀 )
48 1st2ndbr ( ( Rel 𝑀𝑟𝑀 ) → ( 1st𝑟 ) 𝑀 ( 2nd𝑟 ) )
49 46 47 48 syl2anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st𝑟 ) 𝑀 ( 2nd𝑟 ) )
50 xp2nd ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) → ( 2nd𝑟 ) ∈ ( 𝑉 “ { ( 2nd𝑧 ) } ) )
51 36 50 syl ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 2nd𝑟 ) ∈ ( 𝑉 “ { ( 2nd𝑧 ) } ) )
52 elrelimasn ( Rel 𝑉 → ( ( 2nd𝑟 ) ∈ ( 𝑉 “ { ( 2nd𝑧 ) } ) ↔ ( 2nd𝑧 ) 𝑉 ( 2nd𝑟 ) ) )
53 52 biimpa ( ( Rel 𝑉 ∧ ( 2nd𝑟 ) ∈ ( 𝑉 “ { ( 2nd𝑧 ) } ) ) → ( 2nd𝑧 ) 𝑉 ( 2nd𝑟 ) )
54 32 51 53 syl2anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 2nd𝑧 ) 𝑉 ( 2nd𝑟 ) )
55 simpr1r ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑉𝑈 𝑉 = 𝑉 ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) ) → 𝑉 = 𝑉 )
56 55 3anassrs ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑉 = 𝑉 )
57 breq ( 𝑉 = 𝑉 → ( ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ↔ ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ) )
58 fvex ( 2nd𝑟 ) ∈ V
59 fvex ( 2nd𝑧 ) ∈ V
60 58 59 brcnv ( ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ↔ ( 2nd𝑧 ) 𝑉 ( 2nd𝑟 ) )
61 57 60 bitr3di ( 𝑉 = 𝑉 → ( ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ↔ ( 2nd𝑧 ) 𝑉 ( 2nd𝑟 ) ) )
62 56 61 syl ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ↔ ( 2nd𝑧 ) 𝑉 ( 2nd𝑟 ) ) )
63 54 62 mpbird ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) )
64 fvex ( 1st𝑧 ) ∈ V
65 fvex ( 1st𝑟 ) ∈ V
66 brcogw ( ( ( ( 1st𝑧 ) ∈ V ∧ ( 2nd𝑟 ) ∈ V ∧ ( 1st𝑟 ) ∈ V ) ∧ ( ( 1st𝑧 ) 𝑉 ( 1st𝑟 ) ∧ ( 1st𝑟 ) 𝑀 ( 2nd𝑟 ) ) ) → ( 1st𝑧 ) ( 𝑀𝑉 ) ( 2nd𝑟 ) )
67 66 ex ( ( ( 1st𝑧 ) ∈ V ∧ ( 2nd𝑟 ) ∈ V ∧ ( 1st𝑟 ) ∈ V ) → ( ( ( 1st𝑧 ) 𝑉 ( 1st𝑟 ) ∧ ( 1st𝑟 ) 𝑀 ( 2nd𝑟 ) ) → ( 1st𝑧 ) ( 𝑀𝑉 ) ( 2nd𝑟 ) ) )
68 64 58 65 67 mp3an ( ( ( 1st𝑧 ) 𝑉 ( 1st𝑟 ) ∧ ( 1st𝑟 ) 𝑀 ( 2nd𝑟 ) ) → ( 1st𝑧 ) ( 𝑀𝑉 ) ( 2nd𝑟 ) )
69 brcogw ( ( ( ( 1st𝑧 ) ∈ V ∧ ( 2nd𝑧 ) ∈ V ∧ ( 2nd𝑟 ) ∈ V ) ∧ ( ( 1st𝑧 ) ( 𝑀𝑉 ) ( 2nd𝑟 ) ∧ ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ) ) → ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) )
70 69 ex ( ( ( 1st𝑧 ) ∈ V ∧ ( 2nd𝑧 ) ∈ V ∧ ( 2nd𝑟 ) ∈ V ) → ( ( ( 1st𝑧 ) ( 𝑀𝑉 ) ( 2nd𝑟 ) ∧ ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ) → ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) ) )
71 64 59 58 70 mp3an ( ( ( 1st𝑧 ) ( 𝑀𝑉 ) ( 2nd𝑟 ) ∧ ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ) → ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) )
72 68 71 sylan ( ( ( ( 1st𝑧 ) 𝑉 ( 1st𝑟 ) ∧ ( 1st𝑟 ) 𝑀 ( 2nd𝑟 ) ) ∧ ( 2nd𝑟 ) 𝑉 ( 2nd𝑧 ) ) → ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) )
73 41 49 63 72 syl21anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) )
74 73 ralrimiva ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ∀ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) )
75 simplll ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
76 simplrl ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑉𝑈 )
77 4 3ad2ant1 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝑧 ∈ ( 𝑋 × 𝑋 ) ) → 𝐽 ∈ Top )
78 xp1st ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( 1st𝑧 ) ∈ 𝑋 )
79 1 utopsnnei ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ∧ ( 1st𝑧 ) ∈ 𝑋 ) → ( 𝑉 “ { ( 1st𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1st𝑧 ) } ) )
80 78 79 syl3an3 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑉 “ { ( 1st𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1st𝑧 ) } ) )
81 xp2nd ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( 2nd𝑧 ) ∈ 𝑋 )
82 1 utopsnnei ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ∧ ( 2nd𝑧 ) ∈ 𝑋 ) → ( 𝑉 “ { ( 2nd𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2nd𝑧 ) } ) )
83 81 82 syl3an3 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑉 “ { ( 2nd𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2nd𝑧 ) } ) )
84 14 14 neitx ( ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) ∧ ( ( 𝑉 “ { ( 1st𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1st𝑧 ) } ) ∧ ( 𝑉 “ { ( 2nd𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2nd𝑧 ) } ) ) ) → ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st𝑧 ) } × { ( 2nd𝑧 ) } ) ) )
85 77 77 80 83 84 syl22anc ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st𝑧 ) } × { ( 2nd𝑧 ) } ) ) )
86 1st2nd2 ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → 𝑧 = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
87 86 sneqd ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → { 𝑧 } = { ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ } )
88 64 59 xpsn ( { ( 1st𝑧 ) } × { ( 2nd𝑧 ) } ) = { ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ }
89 87 88 eqtr4di ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → { 𝑧 } = ( { ( 1st𝑧 ) } × { ( 2nd𝑧 ) } ) )
90 89 fveq2d ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) = ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st𝑧 ) } × { ( 2nd𝑧 ) } ) ) )
91 90 3ad2ant3 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) = ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st𝑧 ) } × { ( 2nd𝑧 ) } ) ) )
92 85 91 eleqtrrd ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) )
93 75 76 25 92 syl3anc ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) )
94 20 neindisj ( ( ( ( 𝐽 ×t 𝐽 ) ∈ Top ∧ 𝑀 ( 𝐽 ×t 𝐽 ) ) ∧ ( 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ∧ ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) ) ) → ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ≠ ∅ )
95 7 19 24 93 94 syl22anc ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ≠ ∅ )
96 r19.3rzv ( ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ≠ ∅ → ( ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) ↔ ∀ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) ) )
97 95 96 syl ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) ↔ ∀ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st𝑧 ) } ) × ( 𝑉 “ { ( 2nd𝑧 ) } ) ) ∩ 𝑀 ) ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) ) )
98 74 97 mpbird ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) )
99 df-br ( ( 1st𝑧 ) ( 𝑉 ∘ ( 𝑀𝑉 ) ) ( 2nd𝑧 ) ↔ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ∈ ( 𝑉 ∘ ( 𝑀𝑉 ) ) )
100 98 99 sylib ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ∈ ( 𝑉 ∘ ( 𝑀𝑉 ) ) )
101 27 100 eqeltrd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 ∈ ( 𝑉 ∘ ( 𝑀𝑉 ) ) )
102 101 ex ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) → ( 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) → 𝑧 ∈ ( 𝑉 ∘ ( 𝑀𝑉 ) ) ) )
103 102 ssrdv ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉𝑈 𝑉 = 𝑉 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝑉 ∘ ( 𝑀𝑉 ) ) )