MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  utop3cls Structured version   Visualization version   GIF version

Theorem utop3cls 22833
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.)
Hypothesis
Ref Expression
utoptop.1 𝐽 = (unifTop‘𝑈)
Assertion
Ref Expression
utop3cls (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀𝑉)))

Proof of Theorem utop3cls
Dummy variables 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 5547 . . . . 5 Rel (𝑋 × 𝑋)
2 utoptop.1 . . . . . . . . . . 11 𝐽 = (unifTop‘𝑈)
3 utoptop 22816 . . . . . . . . . . 11 (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top)
42, 3eqeltrid 2915 . . . . . . . . . 10 (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ Top)
5 txtop 22150 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
64, 4, 5syl2anc 586 . . . . . . . . 9 (𝑈 ∈ (UnifOn‘𝑋) → (𝐽 ×t 𝐽) ∈ Top)
76ad3antrrr 728 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝐽 ×t 𝐽) ∈ Top)
8 simpllr 774 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋))
9 utoptopon 22818 . . . . . . . . . . . . . 14 (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋))
102, 9eqeltrid 2915 . . . . . . . . . . . . 13 (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
11 toponuni 21495 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
1210, 11syl 17 . . . . . . . . . . . 12 (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = 𝐽)
1312sqxpeqd 5561 . . . . . . . . . . 11 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = ( 𝐽 × 𝐽))
14 eqid 2820 . . . . . . . . . . . . 13 𝐽 = 𝐽
1514, 14txuni 22173 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ( 𝐽 × 𝐽) = (𝐽 ×t 𝐽))
164, 4, 15syl2anc 586 . . . . . . . . . . 11 (𝑈 ∈ (UnifOn‘𝑋) → ( 𝐽 × 𝐽) = (𝐽 ×t 𝐽))
1713, 16eqtrd 2855 . . . . . . . . . 10 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
1817ad3antrrr 728 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
198, 18sseqtrd 3983 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 (𝐽 ×t 𝐽))
20 eqid 2820 . . . . . . . . 9 (𝐽 ×t 𝐽) = (𝐽 ×t 𝐽)
2120clsss3 21640 . . . . . . . 8 (((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 (𝐽 ×t 𝐽)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝐽 ×t 𝐽))
227, 19, 21syl2anc 586 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝐽 ×t 𝐽))
2322, 18sseqtrrd 3984 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑋 × 𝑋))
24 simpr 487 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀))
2523, 24sseldd 3944 . . . . 5 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑋 × 𝑋))
26 1st2nd 7714 . . . . 5 ((Rel (𝑋 × 𝑋) ∧ 𝑧 ∈ (𝑋 × 𝑋)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
271, 25, 26sylancr 589 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
28 simp-4l 781 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑈 ∈ (UnifOn‘𝑋))
29 simpr1l 1226 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉𝑈𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀))) → 𝑉𝑈)
30293anassrs 1356 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑉𝑈)
31 ustrel 22793 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈) → Rel 𝑉)
3228, 30, 31syl2anc 586 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → Rel 𝑉)
33 simpr 487 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀))
34 elin 4145 . . . . . . . . . . . 12 (𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ↔ (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∧ 𝑟𝑀))
3533, 34sylib 220 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∧ 𝑟𝑀))
3635simpld 497 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})))
37 xp1st 7697 . . . . . . . . . 10 (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) → (1st𝑟) ∈ (𝑉 “ {(1st𝑧)}))
3836, 37syl 17 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑟) ∈ (𝑉 “ {(1st𝑧)}))
39 elrelimasn 5927 . . . . . . . . . 10 (Rel 𝑉 → ((1st𝑟) ∈ (𝑉 “ {(1st𝑧)}) ↔ (1st𝑧)𝑉(1st𝑟)))
4039biimpa 479 . . . . . . . . 9 ((Rel 𝑉 ∧ (1st𝑟) ∈ (𝑉 “ {(1st𝑧)})) → (1st𝑧)𝑉(1st𝑟))
4132, 38, 40syl2anc 586 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑧)𝑉(1st𝑟))
42 simp-4r 782 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋))
43 xpss 5545 . . . . . . . . . . 11 (𝑋 × 𝑋) ⊆ (V × V)
4442, 43sstrdi 3955 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (V × V))
45 df-rel 5536 . . . . . . . . . 10 (Rel 𝑀𝑀 ⊆ (V × V))
4644, 45sylibr 236 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → Rel 𝑀)
4735simprd 498 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑟𝑀)
48 1st2ndbr 7717 . . . . . . . . 9 ((Rel 𝑀𝑟𝑀) → (1st𝑟)𝑀(2nd𝑟))
4946, 47, 48syl2anc 586 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑟)𝑀(2nd𝑟))
50 xp2nd 7698 . . . . . . . . . . 11 (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) → (2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)}))
5136, 50syl 17 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)}))
52 elrelimasn 5927 . . . . . . . . . . 11 (Rel 𝑉 → ((2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)}) ↔ (2nd𝑧)𝑉(2nd𝑟)))
5352biimpa 479 . . . . . . . . . 10 ((Rel 𝑉 ∧ (2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)})) → (2nd𝑧)𝑉(2nd𝑟))
5432, 51, 53syl2anc 586 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (2nd𝑧)𝑉(2nd𝑟))
55 simpr1r 1227 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉𝑈𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀))) → 𝑉 = 𝑉)
56553anassrs 1356 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑉 = 𝑉)
57 breq 5042 . . . . . . . . . . 11 (𝑉 = 𝑉 → ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑟)𝑉(2nd𝑧)))
58 fvex 6657 . . . . . . . . . . . 12 (2nd𝑟) ∈ V
59 fvex 6657 . . . . . . . . . . . 12 (2nd𝑧) ∈ V
6058, 59brcnv 5727 . . . . . . . . . . 11 ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑧)𝑉(2nd𝑟))
6157, 60bitr3di 288 . . . . . . . . . 10 (𝑉 = 𝑉 → ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑧)𝑉(2nd𝑟)))
6256, 61syl 17 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑧)𝑉(2nd𝑟)))
6354, 62mpbird 259 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (2nd𝑟)𝑉(2nd𝑧))
64 fvex 6657 . . . . . . . . . 10 (1st𝑧) ∈ V
65 fvex 6657 . . . . . . . . . 10 (1st𝑟) ∈ V
66 brcogw 5713 . . . . . . . . . . 11 ((((1st𝑧) ∈ V ∧ (2nd𝑟) ∈ V ∧ (1st𝑟) ∈ V) ∧ ((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟))) → (1st𝑧)(𝑀𝑉)(2nd𝑟))
6766ex 415 . . . . . . . . . 10 (((1st𝑧) ∈ V ∧ (2nd𝑟) ∈ V ∧ (1st𝑟) ∈ V) → (((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟)) → (1st𝑧)(𝑀𝑉)(2nd𝑟)))
6864, 58, 65, 67mp3an 1457 . . . . . . . . 9 (((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟)) → (1st𝑧)(𝑀𝑉)(2nd𝑟))
69 brcogw 5713 . . . . . . . . . . 11 ((((1st𝑧) ∈ V ∧ (2nd𝑧) ∈ V ∧ (2nd𝑟) ∈ V) ∧ ((1st𝑧)(𝑀𝑉)(2nd𝑟) ∧ (2nd𝑟)𝑉(2nd𝑧))) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7069ex 415 . . . . . . . . . 10 (((1st𝑧) ∈ V ∧ (2nd𝑧) ∈ V ∧ (2nd𝑟) ∈ V) → (((1st𝑧)(𝑀𝑉)(2nd𝑟) ∧ (2nd𝑟)𝑉(2nd𝑧)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧)))
7164, 59, 58, 70mp3an 1457 . . . . . . . . 9 (((1st𝑧)(𝑀𝑉)(2nd𝑟) ∧ (2nd𝑟)𝑉(2nd𝑧)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7268, 71sylan 582 . . . . . . . 8 ((((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟)) ∧ (2nd𝑟)𝑉(2nd𝑧)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7341, 49, 63, 72syl21anc 835 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7473ralrimiva 3169 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ∀𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)(1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
75 simplll 773 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑈 ∈ (UnifOn‘𝑋))
76 simplrl 775 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑉𝑈)
7743ad2ant1 1129 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → 𝐽 ∈ Top)
78 xp1st 7697 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 × 𝑋) → (1st𝑧) ∈ 𝑋)
792utopsnnei 22831 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈 ∧ (1st𝑧) ∈ 𝑋) → (𝑉 “ {(1st𝑧)}) ∈ ((nei‘𝐽)‘{(1st𝑧)}))
8078, 79syl3an3 1161 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(1st𝑧)}) ∈ ((nei‘𝐽)‘{(1st𝑧)}))
81 xp2nd 7698 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 × 𝑋) → (2nd𝑧) ∈ 𝑋)
822utopsnnei 22831 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈 ∧ (2nd𝑧) ∈ 𝑋) → (𝑉 “ {(2nd𝑧)}) ∈ ((nei‘𝐽)‘{(2nd𝑧)}))
8381, 82syl3an3 1161 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(2nd𝑧)}) ∈ ((nei‘𝐽)‘{(2nd𝑧)}))
8414, 14neitx 22188 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 “ {(1st𝑧)}) ∈ ((nei‘𝐽)‘{(1st𝑧)}) ∧ (𝑉 “ {(2nd𝑧)}) ∈ ((nei‘𝐽)‘{(2nd𝑧)}))) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
8577, 77, 80, 83, 84syl22anc 836 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
86 1st2nd2 7704 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑋 × 𝑋) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
8786sneqd 4553 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = {⟨(1st𝑧), (2nd𝑧)⟩})
8864, 59xpsn 6877 . . . . . . . . . . . . 13 ({(1st𝑧)} × {(2nd𝑧)}) = {⟨(1st𝑧), (2nd𝑧)⟩}
8987, 88syl6eqr 2873 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = ({(1st𝑧)} × {(2nd𝑧)}))
9089fveq2d 6648 . . . . . . . . . . 11 (𝑧 ∈ (𝑋 × 𝑋) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
91903ad2ant3 1131 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
9285, 91eleqtrrd 2914 . . . . . . . . 9 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))
9375, 76, 25, 92syl3anc 1367 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))
9420neindisj 21698 . . . . . . . 8 ((((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 (𝐽 ×t 𝐽)) ∧ (𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))) → (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ≠ ∅)
957, 19, 24, 93, 94syl22anc 836 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ≠ ∅)
96 r19.3rzv 4418 . . . . . . 7 ((((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ≠ ∅ → ((1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)(1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧)))
9795, 96syl 17 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)(1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧)))
9874, 97mpbird 259 . . . . 5 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
99 df-br 5041 . . . . 5 ((1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧) ↔ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ (𝑉 ∘ (𝑀𝑉)))
10098, 99sylib 220 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ (𝑉 ∘ (𝑀𝑉)))
10127, 100eqeltrd 2911 . . 3 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑉 ∘ (𝑀𝑉)))
102101ex 415 . 2 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) → (𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) → 𝑧 ∈ (𝑉 ∘ (𝑀𝑉))))
103102ssrdv 3949 1 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀𝑉)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1083   = wceq 1537  wcel 2114  wne 3006  wral 3125  Vcvv 3473  cin 3911  wss 3912  c0 4267  {csn 4541  cop 4547   cuni 4812   class class class wbr 5040   × cxp 5527  ccnv 5528  cima 5532  ccom 5533  Rel wrel 5534  cfv 6329  (class class class)co 7131  1st c1st 7663  2nd c2nd 7664  Topctop 21474  TopOnctopon 21491  clsccl 21599  neicnei 21678   ×t ctx 22141  UnifOncust 22781  unifTopcutop 22812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5240  ax-pr 5304  ax-un 7437
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3752  df-csb 3860  df-dif 3915  df-un 3917  df-in 3919  df-ss 3928  df-pss 3930  df-nul 4268  df-if 4442  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4813  df-int 4851  df-iun 4895  df-iin 4896  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5434  df-eprel 5439  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6122  df-ord 6168  df-on 6169  df-lim 6170  df-suc 6171  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-ov 7134  df-oprab 7135  df-mpo 7136  df-om 7557  df-1st 7665  df-2nd 7666  df-wrecs 7923  df-recs 7984  df-rdg 8022  df-1o 8078  df-oadd 8082  df-er 8265  df-en 8486  df-fin 8489  df-fi 8851  df-topgen 16693  df-top 21475  df-topon 21492  df-bases 21527  df-cld 21600  df-ntr 21601  df-cls 21602  df-nei 21679  df-tx 22143  df-ust 22782  df-utop 22813
This theorem is referenced by:  utopreg  22834
  Copyright terms: Public domain W3C validator