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

Theorem utop3cls 21807
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 5139 . . . . 5 Rel (𝑋 × 𝑋)
2 utoptop.1 . . . . . . . . . . 11 𝐽 = (unifTop‘𝑈)
3 utoptop 21790 . . . . . . . . . . 11 (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top)
42, 3syl5eqel 2691 . . . . . . . . . 10 (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ Top)
5 txtop 21124 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
64, 4, 5syl2anc 690 . . . . . . . . 9 (𝑈 ∈ (UnifOn‘𝑋) → (𝐽 ×t 𝐽) ∈ Top)
76ad3antrrr 761 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝐽 ×t 𝐽) ∈ Top)
8 simpllr 794 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋))
9 utoptopon 21792 . . . . . . . . . . . . . 14 (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋))
102, 9syl5eqel 2691 . . . . . . . . . . . . 13 (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
11 toponuni 20484 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
1210, 11syl 17 . . . . . . . . . . . 12 (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = 𝐽)
1312sqxpeqd 5055 . . . . . . . . . . 11 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = ( 𝐽 × 𝐽))
14 eqid 2609 . . . . . . . . . . . . 13 𝐽 = 𝐽
1514, 14txuni 21147 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ( 𝐽 × 𝐽) = (𝐽 ×t 𝐽))
164, 4, 15syl2anc 690 . . . . . . . . . . 11 (𝑈 ∈ (UnifOn‘𝑋) → ( 𝐽 × 𝐽) = (𝐽 ×t 𝐽))
1713, 16eqtrd 2643 . . . . . . . . . 10 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
1817ad3antrrr 761 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
198, 18sseqtrd 3603 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 (𝐽 ×t 𝐽))
20 eqid 2609 . . . . . . . . 9 (𝐽 ×t 𝐽) = (𝐽 ×t 𝐽)
2120clsss3 20615 . . . . . . . 8 (((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 (𝐽 ×t 𝐽)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝐽 ×t 𝐽))
227, 19, 21syl2anc 690 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝐽 ×t 𝐽))
2322, 18sseqtr4d 3604 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑋 × 𝑋))
24 simpr 475 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀))
2523, 24sseldd 3568 . . . . 5 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑋 × 𝑋))
26 1st2nd 7082 . . . . 5 ((Rel (𝑋 × 𝑋) ∧ 𝑧 ∈ (𝑋 × 𝑋)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
271, 25, 26sylancr 693 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
28 simp-4l 801 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑈 ∈ (UnifOn‘𝑋))
29 simpr1l 1110 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉𝑈𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀))) → 𝑉𝑈)
30293anassrs 1281 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑉𝑈)
31 ustrel 21767 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈) → Rel 𝑉)
3228, 30, 31syl2anc 690 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → Rel 𝑉)
33 simpr 475 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀))
34 elin 3757 . . . . . . . . . . . 12 (𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ↔ (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∧ 𝑟𝑀))
3533, 34sylib 206 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∧ 𝑟𝑀))
3635simpld 473 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})))
37 xp1st 7066 . . . . . . . . . 10 (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) → (1st𝑟) ∈ (𝑉 “ {(1st𝑧)}))
3836, 37syl 17 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑟) ∈ (𝑉 “ {(1st𝑧)}))
39 elrelimasn 5395 . . . . . . . . . 10 (Rel 𝑉 → ((1st𝑟) ∈ (𝑉 “ {(1st𝑧)}) ↔ (1st𝑧)𝑉(1st𝑟)))
4039biimpa 499 . . . . . . . . 9 ((Rel 𝑉 ∧ (1st𝑟) ∈ (𝑉 “ {(1st𝑧)})) → (1st𝑧)𝑉(1st𝑟))
4132, 38, 40syl2anc 690 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑧)𝑉(1st𝑟))
42 simp-4r 802 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋))
43 xpss 5138 . . . . . . . . . . 11 (𝑋 × 𝑋) ⊆ (V × V)
4442, 43syl6ss 3579 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (V × V))
45 df-rel 5035 . . . . . . . . . 10 (Rel 𝑀𝑀 ⊆ (V × V))
4644, 45sylibr 222 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → Rel 𝑀)
4735simprd 477 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑟𝑀)
48 1st2ndbr 7085 . . . . . . . . 9 ((Rel 𝑀𝑟𝑀) → (1st𝑟)𝑀(2nd𝑟))
4946, 47, 48syl2anc 690 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑟)𝑀(2nd𝑟))
50 xp2nd 7067 . . . . . . . . . . 11 (𝑟 ∈ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) → (2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)}))
5136, 50syl 17 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)}))
52 elrelimasn 5395 . . . . . . . . . . 11 (Rel 𝑉 → ((2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)}) ↔ (2nd𝑧)𝑉(2nd𝑟)))
5352biimpa 499 . . . . . . . . . 10 ((Rel 𝑉 ∧ (2nd𝑟) ∈ (𝑉 “ {(2nd𝑧)})) → (2nd𝑧)𝑉(2nd𝑟))
5432, 51, 53syl2anc 690 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (2nd𝑧)𝑉(2nd𝑟))
55 simpr1r 1111 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉𝑈𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀))) → 𝑉 = 𝑉)
56553anassrs 1281 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → 𝑉 = 𝑉)
57 fvex 6098 . . . . . . . . . . . 12 (2nd𝑟) ∈ V
58 fvex 6098 . . . . . . . . . . . 12 (2nd𝑧) ∈ V
5957, 58brcnv 5215 . . . . . . . . . . 11 ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑧)𝑉(2nd𝑟))
60 breq 4579 . . . . . . . . . . 11 (𝑉 = 𝑉 → ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑟)𝑉(2nd𝑧)))
6159, 60syl5rbbr 273 . . . . . . . . . 10 (𝑉 = 𝑉 → ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑧)𝑉(2nd𝑟)))
6256, 61syl 17 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → ((2nd𝑟)𝑉(2nd𝑧) ↔ (2nd𝑧)𝑉(2nd𝑟)))
6354, 62mpbird 245 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (2nd𝑟)𝑉(2nd𝑧))
64 fvex 6098 . . . . . . . . . 10 (1st𝑧) ∈ V
65 fvex 6098 . . . . . . . . . 10 (1st𝑟) ∈ V
66 brcogw 5200 . . . . . . . . . . 11 ((((1st𝑧) ∈ V ∧ (2nd𝑟) ∈ V ∧ (1st𝑟) ∈ V) ∧ ((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟))) → (1st𝑧)(𝑀𝑉)(2nd𝑟))
6766ex 448 . . . . . . . . . 10 (((1st𝑧) ∈ V ∧ (2nd𝑟) ∈ V ∧ (1st𝑟) ∈ V) → (((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟)) → (1st𝑧)(𝑀𝑉)(2nd𝑟)))
6864, 57, 65, 67mp3an 1415 . . . . . . . . 9 (((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟)) → (1st𝑧)(𝑀𝑉)(2nd𝑟))
69 brcogw 5200 . . . . . . . . . . 11 ((((1st𝑧) ∈ V ∧ (2nd𝑧) ∈ V ∧ (2nd𝑟) ∈ V) ∧ ((1st𝑧)(𝑀𝑉)(2nd𝑟) ∧ (2nd𝑟)𝑉(2nd𝑧))) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7069ex 448 . . . . . . . . . 10 (((1st𝑧) ∈ V ∧ (2nd𝑧) ∈ V ∧ (2nd𝑟) ∈ V) → (((1st𝑧)(𝑀𝑉)(2nd𝑟) ∧ (2nd𝑟)𝑉(2nd𝑧)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧)))
7164, 58, 57, 70mp3an 1415 . . . . . . . . 9 (((1st𝑧)(𝑀𝑉)(2nd𝑟) ∧ (2nd𝑟)𝑉(2nd𝑧)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7268, 71sylan 486 . . . . . . . 8 ((((1st𝑧)𝑉(1st𝑟) ∧ (1st𝑟)𝑀(2nd𝑟)) ∧ (2nd𝑟)𝑉(2nd𝑧)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7341, 49, 63, 72syl21anc 1316 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
7473ralrimiva 2948 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ∀𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)(1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
75 simplll 793 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑈 ∈ (UnifOn‘𝑋))
76 simplrl 795 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑉𝑈)
7743ad2ant1 1074 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → 𝐽 ∈ Top)
78 xp1st 7066 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 × 𝑋) → (1st𝑧) ∈ 𝑋)
792utopsnnei 21805 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈 ∧ (1st𝑧) ∈ 𝑋) → (𝑉 “ {(1st𝑧)}) ∈ ((nei‘𝐽)‘{(1st𝑧)}))
8078, 79syl3an3 1352 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(1st𝑧)}) ∈ ((nei‘𝐽)‘{(1st𝑧)}))
81 xp2nd 7067 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 × 𝑋) → (2nd𝑧) ∈ 𝑋)
822utopsnnei 21805 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈 ∧ (2nd𝑧) ∈ 𝑋) → (𝑉 “ {(2nd𝑧)}) ∈ ((nei‘𝐽)‘{(2nd𝑧)}))
8381, 82syl3an3 1352 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(2nd𝑧)}) ∈ ((nei‘𝐽)‘{(2nd𝑧)}))
8414, 14neitx 21162 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 “ {(1st𝑧)}) ∈ ((nei‘𝐽)‘{(1st𝑧)}) ∧ (𝑉 “ {(2nd𝑧)}) ∈ ((nei‘𝐽)‘{(2nd𝑧)}))) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
8577, 77, 80, 83, 84syl22anc 1318 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
86 1st2nd2 7073 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑋 × 𝑋) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
8786sneqd 4136 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = {⟨(1st𝑧), (2nd𝑧)⟩})
8864, 58xpsn 6298 . . . . . . . . . . . . 13 ({(1st𝑧)} × {(2nd𝑧)}) = {⟨(1st𝑧), (2nd𝑧)⟩}
8987, 88syl6eqr 2661 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = ({(1st𝑧)} × {(2nd𝑧)}))
9089fveq2d 6092 . . . . . . . . . . 11 (𝑧 ∈ (𝑋 × 𝑋) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
91903ad2ant3 1076 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st𝑧)} × {(2nd𝑧)})))
9285, 91eleqtrrd 2690 . . . . . . . . 9 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉𝑈𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))
9375, 76, 25, 92syl3anc 1317 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))
9420neindisj 20673 . . . . . . . 8 ((((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 (𝐽 ×t 𝐽)) ∧ (𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ ((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))) → (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ≠ ∅)
957, 19, 24, 93, 94syl22anc 1318 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ≠ ∅)
96 r19.3rzv 4015 . . . . . . 7 ((((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀) ≠ ∅ → ((1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)(1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧)))
9795, 96syl 17 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st𝑧)}) × (𝑉 “ {(2nd𝑧)})) ∩ 𝑀)(1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧)))
9874, 97mpbird 245 . . . . 5 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧))
99 df-br 4578 . . . . 5 ((1st𝑧)(𝑉 ∘ (𝑀𝑉))(2nd𝑧) ↔ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ (𝑉 ∘ (𝑀𝑉)))
10098, 99sylib 206 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ (𝑉 ∘ (𝑀𝑉)))
10127, 100eqeltrd 2687 . . 3 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑉 ∘ (𝑀𝑉)))
102101ex 448 . 2 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) → (𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) → 𝑧 ∈ (𝑉 ∘ (𝑀𝑉))))
103102ssrdv 3573 1 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉𝑈𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀𝑉)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  Vcvv 3172  cin 3538  wss 3539  c0 3873  {csn 4124  cop 4130   cuni 4366   class class class wbr 4577   × cxp 5026  ccnv 5027  cima 5031  ccom 5032  Rel wrel 5033  cfv 5790  (class class class)co 6527  1st c1st 7034  2nd c2nd 7035  Topctop 20459  TopOnctopon 20460  clsccl 20574  neicnei 20653   ×t ctx 21115  UnifOncust 21755  unifTopcutop 21786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-en 7819  df-fin 7822  df-fi 8177  df-topgen 15873  df-top 20463  df-bases 20464  df-topon 20465  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-tx 21117  df-ust 21756  df-utop 21787
This theorem is referenced by:  utopreg  21808
  Copyright terms: Public domain W3C validator