| Step | Hyp | Ref
| Expression |
| 1 | | utoptop.1 |
. . . . . . . 8
⊢ 𝐽 = (unifTop‘𝑈) |
| 2 | | utoptop 24243 |
. . . . . . . 8
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top) |
| 3 | 1, 2 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ Top) |
| 4 | | txtop 23577 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top) |
| 5 | 3, 3, 4 | syl2anc 584 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐽 ×t 𝐽) ∈ Top) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝐽 ×t 𝐽) ∈ Top) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → (𝐽 ×t 𝐽) ∈ Top) |
| 8 | | 0nei 23136 |
. . . 4
⊢ ((𝐽 ×t 𝐽) ∈ Top → ∅
∈ ((nei‘(𝐽
×t 𝐽))‘∅)) |
| 9 | 7, 8 | syl 17 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → ∅ ∈
((nei‘(𝐽
×t 𝐽))‘∅)) |
| 10 | | coeq1 5868 |
. . . . . . 7
⊢ (𝑀 = ∅ → (𝑀 ∘ 𝑉) = (∅ ∘ 𝑉)) |
| 11 | | co01 6281 |
. . . . . . 7
⊢ (∅
∘ 𝑉) =
∅ |
| 12 | 10, 11 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑀 = ∅ → (𝑀 ∘ 𝑉) = ∅) |
| 13 | 12 | coeq2d 5873 |
. . . . 5
⊢ (𝑀 = ∅ → (𝑉 ∘ (𝑀 ∘ 𝑉)) = (𝑉 ∘ ∅)) |
| 14 | | co02 6280 |
. . . . 5
⊢ (𝑉 ∘ ∅) =
∅ |
| 15 | 13, 14 | eqtrdi 2793 |
. . . 4
⊢ (𝑀 = ∅ → (𝑉 ∘ (𝑀 ∘ 𝑉)) = ∅) |
| 16 | 15 | adantl 481 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → (𝑉 ∘ (𝑀 ∘ 𝑉)) = ∅) |
| 17 | | simpr 484 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → 𝑀 = ∅) |
| 18 | 17 | fveq2d 6910 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → ((nei‘(𝐽 ×t 𝐽))‘𝑀) = ((nei‘(𝐽 ×t 𝐽))‘∅)) |
| 19 | 9, 16, 18 | 3eltr4d 2856 |
. 2
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀)) |
| 20 | 6 | adantr 480 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝐽 ×t 𝐽) ∈ Top) |
| 21 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑈 ∈ (UnifOn‘𝑋)) |
| 22 | 21, 3 | syl 17 |
. . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝐽 ∈ Top) |
| 23 | | simpl2l 1227 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑉 ∈ 𝑈) |
| 24 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑀 ⊆ (𝑋 × 𝑋)) |
| 25 | 24 | sselda 3983 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑟 ∈ (𝑋 × 𝑋)) |
| 26 | | xp1st 8046 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ (𝑋 × 𝑋) → (1st ‘𝑟) ∈ 𝑋) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (1st ‘𝑟) ∈ 𝑋) |
| 28 | 1 | utopsnnei 24258 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (1st ‘𝑟) ∈ 𝑋) → (𝑉 “ {(1st ‘𝑟)}) ∈ ((nei‘𝐽)‘{(1st
‘𝑟)})) |
| 29 | 21, 23, 27, 28 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 “ {(1st ‘𝑟)}) ∈ ((nei‘𝐽)‘{(1st
‘𝑟)})) |
| 30 | | xp2nd 8047 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ (𝑋 × 𝑋) → (2nd ‘𝑟) ∈ 𝑋) |
| 31 | 25, 30 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (2nd ‘𝑟) ∈ 𝑋) |
| 32 | 1 | utopsnnei 24258 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (2nd ‘𝑟) ∈ 𝑋) → (𝑉 “ {(2nd ‘𝑟)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑟)})) |
| 33 | 21, 23, 31, 32 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 “ {(2nd ‘𝑟)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑟)})) |
| 34 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 35 | 34, 34 | neitx 23615 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 “ {(1st
‘𝑟)}) ∈
((nei‘𝐽)‘{(1st ‘𝑟)}) ∧ (𝑉 “ {(2nd ‘𝑟)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑟)}))) →
((𝑉 “
{(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st
‘𝑟)} ×
{(2nd ‘𝑟)}))) |
| 36 | 22, 22, 29, 33, 35 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st
‘𝑟)} ×
{(2nd ‘𝑟)}))) |
| 37 | | fvex 6919 |
. . . . . . . . . 10
⊢
(1st ‘𝑟) ∈ V |
| 38 | | fvex 6919 |
. . . . . . . . . 10
⊢
(2nd ‘𝑟) ∈ V |
| 39 | 37, 38 | xpsn 7161 |
. . . . . . . . 9
⊢
({(1st ‘𝑟)} × {(2nd ‘𝑟)}) = {〈(1st
‘𝑟), (2nd
‘𝑟)〉} |
| 40 | 39 | fveq2i 6909 |
. . . . . . . 8
⊢
((nei‘(𝐽
×t 𝐽))‘({(1st ‘𝑟)} × {(2nd
‘𝑟)})) =
((nei‘(𝐽
×t 𝐽))‘{〈(1st ‘𝑟), (2nd ‘𝑟)〉}) |
| 41 | 36, 40 | eleqtrdi 2851 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{〈(1st
‘𝑟), (2nd
‘𝑟)〉})) |
| 42 | 24 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑀 ⊆ (𝑋 × 𝑋)) |
| 43 | | xpss 5701 |
. . . . . . . . . . . . 13
⊢ (𝑋 × 𝑋) ⊆ (V × V) |
| 44 | | sstr 3992 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ⊆ (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ⊆ (V × V)) → 𝑀 ⊆ (V ×
V)) |
| 45 | 43, 44 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑀 ⊆ (𝑋 × 𝑋) → 𝑀 ⊆ (V × V)) |
| 46 | | df-rel 5692 |
. . . . . . . . . . . 12
⊢ (Rel
𝑀 ↔ 𝑀 ⊆ (V × V)) |
| 47 | 45, 46 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝑀 ⊆ (𝑋 × 𝑋) → Rel 𝑀) |
| 48 | 42, 47 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → Rel 𝑀) |
| 49 | | 1st2nd 8064 |
. . . . . . . . . 10
⊢ ((Rel
𝑀 ∧ 𝑟 ∈ 𝑀) → 𝑟 = 〈(1st ‘𝑟), (2nd ‘𝑟)〉) |
| 50 | 48, 49 | sylancom 588 |
. . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑟 = 〈(1st ‘𝑟), (2nd ‘𝑟)〉) |
| 51 | 50 | sneqd 4638 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → {𝑟} = {〈(1st ‘𝑟), (2nd ‘𝑟)〉}) |
| 52 | 51 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((nei‘(𝐽 ×t 𝐽))‘{𝑟}) = ((nei‘(𝐽 ×t 𝐽))‘{〈(1st ‘𝑟), (2nd ‘𝑟)〉})) |
| 53 | 41, 52 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑟})) |
| 54 | | relxp 5703 |
. . . . . . . . . . 11
⊢ Rel
((𝑉 “
{(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) |
| 55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → Rel ((𝑉 “ {(1st
‘𝑟)}) × (𝑉 “ {(2nd
‘𝑟)}))) |
| 56 | | 1st2nd 8064 |
. . . . . . . . . 10
⊢ ((Rel
((𝑉 “
{(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 57 | 55, 56 | sylancom 588 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 58 | | simpll2 1214 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) |
| 59 | 58 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → ◡𝑉 = 𝑉) |
| 60 | | simpll1 1213 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → 𝑈 ∈ (UnifOn‘𝑋)) |
| 61 | 58 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → 𝑉 ∈ 𝑈) |
| 62 | | ustrel 24220 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉) |
| 63 | 60, 61, 62 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → Rel 𝑉) |
| 64 | | xp1st 8046 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) → (1st
‘𝑧) ∈ (𝑉 “ {(1st
‘𝑟)})) |
| 65 | 64 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (1st
‘𝑧) ∈ (𝑉 “ {(1st
‘𝑟)})) |
| 66 | | elrelimasn 6104 |
. . . . . . . . . . . . . 14
⊢ (Rel
𝑉 → ((1st
‘𝑧) ∈ (𝑉 “ {(1st
‘𝑟)}) ↔
(1st ‘𝑟)𝑉(1st ‘𝑧))) |
| 67 | 66 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ ((Rel
𝑉 ∧ (1st
‘𝑧) ∈ (𝑉 “ {(1st
‘𝑟)})) →
(1st ‘𝑟)𝑉(1st ‘𝑧)) |
| 68 | 63, 65, 67 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (1st
‘𝑟)𝑉(1st ‘𝑧)) |
| 69 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(1st ‘𝑧) ∈ V |
| 70 | 37, 69 | brcnv 5893 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑟)◡𝑉(1st ‘𝑧) ↔ (1st ‘𝑧)𝑉(1st ‘𝑟)) |
| 71 | | breq 5145 |
. . . . . . . . . . . . . 14
⊢ (◡𝑉 = 𝑉 → ((1st ‘𝑟)◡𝑉(1st ‘𝑧) ↔ (1st ‘𝑟)𝑉(1st ‘𝑧))) |
| 72 | 70, 71 | bitr3id 285 |
. . . . . . . . . . . . 13
⊢ (◡𝑉 = 𝑉 → ((1st ‘𝑧)𝑉(1st ‘𝑟) ↔ (1st ‘𝑟)𝑉(1st ‘𝑧))) |
| 73 | 72 | biimpar 477 |
. . . . . . . . . . . 12
⊢ ((◡𝑉 = 𝑉 ∧ (1st ‘𝑟)𝑉(1st ‘𝑧)) → (1st ‘𝑧)𝑉(1st ‘𝑟)) |
| 74 | 59, 68, 73 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (1st
‘𝑧)𝑉(1st ‘𝑟)) |
| 75 | | simpll3 1215 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → 𝑀 ⊆ (𝑋 × 𝑋)) |
| 76 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → 𝑟 ∈ 𝑀) |
| 77 | | 1st2ndbr 8067 |
. . . . . . . . . . . . 13
⊢ ((Rel
𝑀 ∧ 𝑟 ∈ 𝑀) → (1st ‘𝑟)𝑀(2nd ‘𝑟)) |
| 78 | 47, 77 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝑀 ⊆ (𝑋 × 𝑋) ∧ 𝑟 ∈ 𝑀) → (1st ‘𝑟)𝑀(2nd ‘𝑟)) |
| 79 | 75, 76, 78 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (1st
‘𝑟)𝑀(2nd ‘𝑟)) |
| 80 | | xp2nd 8047 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) → (2nd
‘𝑧) ∈ (𝑉 “ {(2nd
‘𝑟)})) |
| 81 | 80 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (2nd
‘𝑧) ∈ (𝑉 “ {(2nd
‘𝑟)})) |
| 82 | | elrelimasn 6104 |
. . . . . . . . . . . . 13
⊢ (Rel
𝑉 → ((2nd
‘𝑧) ∈ (𝑉 “ {(2nd
‘𝑟)}) ↔
(2nd ‘𝑟)𝑉(2nd ‘𝑧))) |
| 83 | 82 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((Rel
𝑉 ∧ (2nd
‘𝑧) ∈ (𝑉 “ {(2nd
‘𝑟)})) →
(2nd ‘𝑟)𝑉(2nd ‘𝑧)) |
| 84 | 63, 81, 83 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (2nd
‘𝑟)𝑉(2nd ‘𝑧)) |
| 85 | 69, 38, 37 | 3pm3.2i 1340 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑟) ∈ V ∧ (1st
‘𝑟) ∈
V) |
| 86 | | brcogw 5879 |
. . . . . . . . . . . . 13
⊢
((((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑟) ∈ V ∧ (1st
‘𝑟) ∈ V) ∧
((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟))) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟)) |
| 87 | 85, 86 | mpan 690 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟)) |
| 88 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘𝑧) ∈ V |
| 89 | 69, 88, 38 | 3pm3.2i 1340 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑧) ∈ V ∧ (2nd
‘𝑟) ∈
V) |
| 90 | | brcogw 5879 |
. . . . . . . . . . . . 13
⊢
((((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑧) ∈ V ∧ (2nd
‘𝑟) ∈ V) ∧
((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧))) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 91 | 89, 90 | mpan 690 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 92 | 87, 91 | sylan 580 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 93 | 74, 79, 84, 92 | syl21anc 838 |
. . . . . . . . . 10
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → (1st
‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
| 94 | | df-br 5144 |
. . . . . . . . . 10
⊢
((1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧) ↔ 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
| 95 | 93, 94 | sylib 218 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) →
〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
| 96 | 57, 95 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)}))) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
| 97 | 96 | ex 412 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑧 ∈ ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))) |
| 98 | 97 | ssrdv 3989 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
| 99 | | simp1 1137 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑈 ∈ (UnifOn‘𝑋)) |
| 100 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑉 ∈ 𝑈) |
| 101 | | ustssxp 24213 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋)) |
| 102 | 99, 100, 101 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑉 ⊆ (𝑋 × 𝑋)) |
| 103 | | coss1 5866 |
. . . . . . . . . 10
⊢ (𝑉 ⊆ (𝑋 × 𝑋) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉))) |
| 104 | 102, 103 | syl 17 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉))) |
| 105 | | coss1 5866 |
. . . . . . . . . . . 12
⊢ (𝑀 ⊆ (𝑋 × 𝑋) → (𝑀 ∘ 𝑉) ⊆ ((𝑋 × 𝑋) ∘ 𝑉)) |
| 106 | 24, 105 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑀 ∘ 𝑉) ⊆ ((𝑋 × 𝑋) ∘ 𝑉)) |
| 107 | | coss2 5867 |
. . . . . . . . . . . . 13
⊢ (𝑉 ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ 𝑉) ⊆ ((𝑋 × 𝑋) ∘ (𝑋 × 𝑋))) |
| 108 | | xpcoid 6310 |
. . . . . . . . . . . . 13
⊢ ((𝑋 × 𝑋) ∘ (𝑋 × 𝑋)) = (𝑋 × 𝑋) |
| 109 | 107, 108 | sseqtrdi 4024 |
. . . . . . . . . . . 12
⊢ (𝑉 ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ 𝑉) ⊆ (𝑋 × 𝑋)) |
| 110 | 102, 109 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → ((𝑋 × 𝑋) ∘ 𝑉) ⊆ (𝑋 × 𝑋)) |
| 111 | 106, 110 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑀 ∘ 𝑉) ⊆ (𝑋 × 𝑋)) |
| 112 | | coss2 5867 |
. . . . . . . . . . 11
⊢ ((𝑀 ∘ 𝑉) ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)) ⊆ ((𝑋 × 𝑋) ∘ (𝑋 × 𝑋))) |
| 113 | 112, 108 | sseqtrdi 4024 |
. . . . . . . . . 10
⊢ ((𝑀 ∘ 𝑉) ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)) ⊆ (𝑋 × 𝑋)) |
| 114 | 111, 113 | syl 17 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)) ⊆ (𝑋 × 𝑋)) |
| 115 | 104, 114 | sstrd 3994 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ (𝑋 × 𝑋)) |
| 116 | | utopbas 24244 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪
(unifTop‘𝑈)) |
| 117 | 1 | unieqi 4919 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ (unifTop‘𝑈) |
| 118 | 116, 117 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 119 | 118 | sqxpeqd 5717 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)) |
| 120 | 34, 34 | txuni 23600 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (∪ 𝐽
× ∪ 𝐽) = ∪ (𝐽 ×t 𝐽)) |
| 121 | 3, 3, 120 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (∪ 𝐽
× ∪ 𝐽) = ∪ (𝐽 ×t 𝐽)) |
| 122 | 119, 121 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
| 123 | 122 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
| 124 | 115, 123 | sseqtrd 4020 |
. . . . . . 7
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ∪
(𝐽 ×t
𝐽)) |
| 125 | 124 | adantr 480 |
. . . . . 6
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ∪
(𝐽 ×t
𝐽)) |
| 126 | | eqid 2737 |
. . . . . . 7
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
| 127 | 126 | ssnei2 23124 |
. . . . . 6
⊢ ((((𝐽 ×t 𝐽) ∈ Top ∧ ((𝑉 “ {(1st
‘𝑟)}) × (𝑉 “ {(2nd
‘𝑟)})) ∈
((nei‘(𝐽
×t 𝐽))‘{𝑟})) ∧ (((𝑉 “ {(1st ‘𝑟)}) × (𝑉 “ {(2nd ‘𝑟)})) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∧ (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ∪
(𝐽 ×t
𝐽))) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑟})) |
| 128 | 20, 53, 98, 125, 127 | syl22anc 839 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑟})) |
| 129 | 128 | ralrimiva 3146 |
. . . 4
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑟})) |
| 130 | 129 | adantr 480 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑟})) |
| 131 | 6 | adantr 480 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → (𝐽 ×t 𝐽) ∈ Top) |
| 132 | 24, 123 | sseqtrd 4020 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑀 ⊆ ∪ (𝐽 ×t 𝐽)) |
| 133 | 132 | adantr 480 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → 𝑀 ⊆ ∪ (𝐽 ×t 𝐽)) |
| 134 | | simpr 484 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → 𝑀 ≠ ∅) |
| 135 | 126 | neips 23121 |
. . . 4
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 ⊆ ∪ (𝐽
×t 𝐽)
∧ 𝑀 ≠ ∅)
→ ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀) ↔ ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑟}))) |
| 136 | 131, 133,
134, 135 | syl3anc 1373 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀) ↔ ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑟}))) |
| 137 | 130, 136 | mpbird 257 |
. 2
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀)) |
| 138 | 19, 137 | pm2.61dane 3029 |
1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀)) |