| Step | Hyp | Ref
| Expression |
| 1 | | relxp 5703 |
. . . . 5
⊢ Rel
(𝑋 × 𝑋) |
| 2 | | utoptop.1 |
. . . . . . . . . . 11
⊢ 𝐽 = (unifTop‘𝑈) |
| 3 | | utoptop 24243 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top) |
| 4 | 2, 3 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ Top) |
| 5 | | txtop 23577 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top) |
| 6 | 4, 4, 5 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐽 ×t 𝐽) ∈ Top) |
| 7 | 6 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝐽 ×t 𝐽) ∈ Top) |
| 8 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋)) |
| 9 | | utoptopon 24245 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋)) |
| 10 | 2, 9 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
| 11 | | toponuni 22920 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 13 | 12 | sqxpeqd 5717 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)) |
| 14 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 15 | 14, 14 | txuni 23600 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (∪ 𝐽
× ∪ 𝐽) = ∪ (𝐽 ×t 𝐽)) |
| 16 | 4, 4, 15 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (∪ 𝐽
× ∪ 𝐽) = ∪ (𝐽 ×t 𝐽)) |
| 17 | 13, 16 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
| 18 | 17 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
| 19 | 8, 18 | sseqtrd 4020 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 ⊆ ∪ (𝐽 ×t 𝐽)) |
| 20 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
| 21 | 20 | clsss3 23067 |
. . . . . . . 8
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 ⊆ ∪ (𝐽
×t 𝐽))
→ ((cls‘(𝐽
×t 𝐽))‘𝑀) ⊆ ∪
(𝐽 ×t
𝐽)) |
| 22 | 7, 19, 21 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ ∪
(𝐽 ×t
𝐽)) |
| 23 | 22, 18 | sseqtrrd 4021 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑋 × 𝑋)) |
| 24 | | simpr 484 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) |
| 25 | 23, 24 | sseldd 3984 |
. . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑋 × 𝑋)) |
| 26 | | 1st2nd 8064 |
. . . . 5
⊢ ((Rel
(𝑋 × 𝑋) ∧ 𝑧 ∈ (𝑋 × 𝑋)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 27 | 1, 25, 26 | sylancr 587 |
. . . 4
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 28 | | simp-4l 783 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑈 ∈ (UnifOn‘𝑋)) |
| 29 | | simpr1l 1231 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀))) → 𝑉 ∈ 𝑈) |
| 30 | 29 | 3anassrs 1361 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑉 ∈ 𝑈) |
| 31 | | ustrel 24220 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉) |
| 32 | 28, 30, 31 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → Rel 𝑉) |
| 33 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) |
| 34 | | elin 3967 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀) ↔ (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∧ 𝑟 ∈ 𝑀)) |
| 35 | 33, 34 | sylib 218 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∧ 𝑟 ∈ 𝑀)) |
| 36 | 35 | simpld 494 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)}))) |
| 37 | | xp1st 8046 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) → (1st
‘𝑟) ∈ (𝑉 “ {(1st
‘𝑧)})) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑟) ∈ (𝑉 “ {(1st ‘𝑧)})) |
| 39 | | elrelimasn 6104 |
. . . . . . . . . 10
⊢ (Rel
𝑉 → ((1st
‘𝑟) ∈ (𝑉 “ {(1st
‘𝑧)}) ↔
(1st ‘𝑧)𝑉(1st ‘𝑟))) |
| 40 | 39 | biimpa 476 |
. . . . . . . . 9
⊢ ((Rel
𝑉 ∧ (1st
‘𝑟) ∈ (𝑉 “ {(1st
‘𝑧)})) →
(1st ‘𝑧)𝑉(1st ‘𝑟)) |
| 41 | 32, 38, 40 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑧)𝑉(1st ‘𝑟)) |
| 42 | | simp-4r 784 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋)) |
| 43 | | xpss 5701 |
. . . . . . . . . . 11
⊢ (𝑋 × 𝑋) ⊆ (V × V) |
| 44 | 42, 43 | sstrdi 3996 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (V × V)) |
| 45 | | df-rel 5692 |
. . . . . . . . . 10
⊢ (Rel
𝑀 ↔ 𝑀 ⊆ (V × V)) |
| 46 | 44, 45 | sylibr 234 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → Rel 𝑀) |
| 47 | 35 | simprd 495 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑟 ∈ 𝑀) |
| 48 | | 1st2ndbr 8067 |
. . . . . . . . 9
⊢ ((Rel
𝑀 ∧ 𝑟 ∈ 𝑀) → (1st ‘𝑟)𝑀(2nd ‘𝑟)) |
| 49 | 46, 47, 48 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑟)𝑀(2nd ‘𝑟)) |
| 50 | | xp2nd 8047 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) → (2nd
‘𝑟) ∈ (𝑉 “ {(2nd
‘𝑧)})) |
| 51 | 36, 50 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (2nd ‘𝑟) ∈ (𝑉 “ {(2nd ‘𝑧)})) |
| 52 | | elrelimasn 6104 |
. . . . . . . . . . 11
⊢ (Rel
𝑉 → ((2nd
‘𝑟) ∈ (𝑉 “ {(2nd
‘𝑧)}) ↔
(2nd ‘𝑧)𝑉(2nd ‘𝑟))) |
| 53 | 52 | biimpa 476 |
. . . . . . . . . 10
⊢ ((Rel
𝑉 ∧ (2nd
‘𝑟) ∈ (𝑉 “ {(2nd
‘𝑧)})) →
(2nd ‘𝑧)𝑉(2nd ‘𝑟)) |
| 54 | 32, 51, 53 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (2nd ‘𝑧)𝑉(2nd ‘𝑟)) |
| 55 | | simpr1r 1232 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀))) → ◡𝑉 = 𝑉) |
| 56 | 55 | 3anassrs 1361 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → ◡𝑉 = 𝑉) |
| 57 | | breq 5145 |
. . . . . . . . . . 11
⊢ (◡𝑉 = 𝑉 → ((2nd ‘𝑟)◡𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑟)𝑉(2nd ‘𝑧))) |
| 58 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑟) ∈ V |
| 59 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑧) ∈ V |
| 60 | 58, 59 | brcnv 5893 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑟)◡𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑧)𝑉(2nd ‘𝑟)) |
| 61 | 57, 60 | bitr3di 286 |
. . . . . . . . . 10
⊢ (◡𝑉 = 𝑉 → ((2nd ‘𝑟)𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑧)𝑉(2nd ‘𝑟))) |
| 62 | 56, 61 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → ((2nd ‘𝑟)𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑧)𝑉(2nd ‘𝑟))) |
| 63 | 54, 62 | mpbird 257 |
. . . . . . . 8
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (2nd ‘𝑟)𝑉(2nd ‘𝑧)) |
| 64 | | fvex 6919 |
. . . . . . . . . 10
⊢
(1st ‘𝑧) ∈ V |
| 65 | | fvex 6919 |
. . . . . . . . . 10
⊢
(1st ‘𝑟) ∈ V |
| 66 | | brcogw 5879 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑟) ∈ V ∧ (1st
‘𝑟) ∈ V) ∧
((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟))) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟)) |
| 67 | 66 | ex 412 |
. . . . . . . . . 10
⊢
(((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑟) ∈ V ∧ (1st
‘𝑟) ∈ V) →
(((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟))) |
| 68 | 64, 58, 65, 67 | mp3an 1463 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟)) |
| 69 | | brcogw 5879 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑧) ∈ V ∧ (2nd
‘𝑟) ∈ V) ∧
((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧))) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 70 | 69 | ex 412 |
. . . . . . . . . 10
⊢
(((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑧) ∈ V ∧ (2nd
‘𝑟) ∈ V) →
(((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧))) |
| 71 | 64, 59, 58, 70 | mp3an 1463 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 72 | 68, 71 | sylan 580 |
. . . . . . . 8
⊢
((((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 73 | 41, 49, 63, 72 | syl21anc 838 |
. . . . . . 7
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 74 | 73 | ralrimiva 3146 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ∀𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)(1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 75 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑈 ∈ (UnifOn‘𝑋)) |
| 76 | | simplrl 777 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑉 ∈ 𝑈) |
| 77 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → 𝐽 ∈ Top) |
| 78 | | xp1st 8046 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑋) → (1st ‘𝑧) ∈ 𝑋) |
| 79 | 2 | utopsnnei 24258 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (1st ‘𝑧) ∈ 𝑋) → (𝑉 “ {(1st ‘𝑧)}) ∈ ((nei‘𝐽)‘{(1st
‘𝑧)})) |
| 80 | 78, 79 | syl3an3 1166 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(1st ‘𝑧)}) ∈ ((nei‘𝐽)‘{(1st
‘𝑧)})) |
| 81 | | xp2nd 8047 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑋) → (2nd ‘𝑧) ∈ 𝑋) |
| 82 | 2 | utopsnnei 24258 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (2nd ‘𝑧) ∈ 𝑋) → (𝑉 “ {(2nd ‘𝑧)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑧)})) |
| 83 | 81, 82 | syl3an3 1166 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(2nd ‘𝑧)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑧)})) |
| 84 | 14, 14 | neitx 23615 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 “ {(1st
‘𝑧)}) ∈
((nei‘𝐽)‘{(1st ‘𝑧)}) ∧ (𝑉 “ {(2nd ‘𝑧)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑧)}))) →
((𝑉 “
{(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st
‘𝑧)} ×
{(2nd ‘𝑧)}))) |
| 85 | 77, 77, 80, 83, 84 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st
‘𝑧)} ×
{(2nd ‘𝑧)}))) |
| 86 | | 1st2nd2 8053 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑋 × 𝑋) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 87 | 86 | sneqd 4638 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = {〈(1st ‘𝑧), (2nd ‘𝑧)〉}) |
| 88 | 64, 59 | xpsn 7161 |
. . . . . . . . . . . . 13
⊢
({(1st ‘𝑧)} × {(2nd ‘𝑧)}) = {〈(1st
‘𝑧), (2nd
‘𝑧)〉} |
| 89 | 87, 88 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = ({(1st ‘𝑧)} × {(2nd
‘𝑧)})) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋 × 𝑋) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st ‘𝑧)} × {(2nd
‘𝑧)}))) |
| 91 | 90 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st ‘𝑧)} × {(2nd
‘𝑧)}))) |
| 92 | 85, 91 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧})) |
| 93 | 75, 76, 25, 92 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧})) |
| 94 | 20 | neindisj 23125 |
. . . . . . . 8
⊢ ((((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 ⊆ ∪ (𝐽
×t 𝐽))
∧ (𝑧 ∈
((cls‘(𝐽
×t 𝐽))‘𝑀) ∧ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))) → (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀) ≠ ∅) |
| 95 | 7, 19, 24, 93, 94 | syl22anc 839 |
. . . . . . 7
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀) ≠ ∅) |
| 96 | | r19.3rzv 4499 |
. . . . . . 7
⊢ ((((𝑉 “ {(1st
‘𝑧)}) × (𝑉 “ {(2nd
‘𝑧)})) ∩ 𝑀) ≠ ∅ →
((1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)(1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧))) |
| 97 | 95, 96 | syl 17 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)(1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧))) |
| 98 | 74, 97 | mpbird 257 |
. . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 99 | | df-br 5144 |
. . . . 5
⊢
((1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧) ↔ 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
| 100 | 98, 99 | sylib 218 |
. . . 4
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
| 101 | 27, 100 | eqeltrd 2841 |
. . 3
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
| 102 | 101 | ex 412 |
. 2
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) → (𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))) |
| 103 | 102 | ssrdv 3989 |
1
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉))) |