| Step | Hyp | Ref
| Expression |
| 1 | | haustop 23339 |
. . 3
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
| 2 | 1 | adantr 480 |
. 2
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) → 𝐽 ∈ Top) |
| 3 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 4 | | eqid 2737 |
. . . . . 6
⊢ {𝑧 ∈ 𝐽 ∣ ∃𝑣 ∈ 𝐽 (𝑦 ∈ 𝑣 ∧ ((cls‘𝐽)‘𝑣) ⊆ (∪ 𝐽 ∖ 𝑧))} = {𝑧 ∈ 𝐽 ∣ ∃𝑣 ∈ 𝐽 (𝑦 ∈ 𝑣 ∧ ((cls‘𝐽)‘𝑣) ⊆ (∪ 𝐽 ∖ 𝑧))} |
| 5 | | simpll 767 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Haus) |
| 6 | | difssd 4137 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (∪ 𝐽 ∖ 𝑥) ⊆ ∪ 𝐽) |
| 7 | | simplr 769 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Comp) |
| 8 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Top) |
| 9 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐽) |
| 10 | 3 | opncld 23041 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽) → (∪ 𝐽 ∖ 𝑥) ∈ (Clsd‘𝐽)) |
| 11 | 8, 9, 10 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (∪ 𝐽 ∖ 𝑥) ∈ (Clsd‘𝐽)) |
| 12 | | cmpcld 23410 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ (∪ 𝐽
∖ 𝑥) ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
(∪ 𝐽 ∖ 𝑥)) ∈ Comp) |
| 13 | 7, 11, 12 | syl2anc 584 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (𝐽 ↾t (∪ 𝐽
∖ 𝑥)) ∈
Comp) |
| 14 | | simprr 773 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑥) |
| 15 | | elssuni 4937 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
| 16 | 15 | ad2antrl 728 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ⊆ ∪ 𝐽) |
| 17 | | dfss4 4269 |
. . . . . . . 8
⊢ (𝑥 ⊆ ∪ 𝐽
↔ (∪ 𝐽 ∖ (∪ 𝐽 ∖ 𝑥)) = 𝑥) |
| 18 | 16, 17 | sylib 218 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑥)) = 𝑥) |
| 19 | 14, 18 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑥))) |
| 20 | 3, 4, 5, 6, 13, 19 | hauscmplem 23414 |
. . . . 5
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑥)))) |
| 21 | 18 | sseq2d 4016 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (((cls‘𝐽)‘𝑢) ⊆ (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑥)) ↔
((cls‘𝐽)‘𝑢) ⊆ 𝑥)) |
| 22 | 21 | anbi2d 630 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ((𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑥))) ↔ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) |
| 23 | 22 | rexbidv 3179 |
. . . . 5
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑥))) ↔
∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) |
| 24 | 20, 23 | mpbid 232 |
. . . 4
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥)) |
| 25 | 8 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → 𝐽 ∈ Top) |
| 26 | | simprl 771 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → 𝑢 ∈ 𝐽) |
| 27 | | simprrl 781 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → 𝑦 ∈ 𝑢) |
| 28 | | opnneip 23127 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢) → 𝑢 ∈ ((nei‘𝐽)‘{𝑦})) |
| 29 | 25, 26, 27, 28 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → 𝑢 ∈ ((nei‘𝐽)‘{𝑦})) |
| 30 | | elssuni 4937 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽) |
| 31 | 30 | ad2antrl 728 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → 𝑢 ⊆ ∪ 𝐽) |
| 32 | 3 | sscls 23064 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽)
→ 𝑢 ⊆
((cls‘𝐽)‘𝑢)) |
| 33 | 25, 31, 32 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢)) |
| 34 | 3 | clsss3 23067 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑢) ⊆ ∪ 𝐽) |
| 35 | 25, 31, 34 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → ((cls‘𝐽)‘𝑢) ⊆ ∪ 𝐽) |
| 36 | 3 | ssnei2 23124 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑢 ∈ ((nei‘𝐽)‘{𝑦})) ∧ (𝑢 ⊆ ((cls‘𝐽)‘𝑢) ∧ ((cls‘𝐽)‘𝑢) ⊆ ∪ 𝐽)) → ((cls‘𝐽)‘𝑢) ∈ ((nei‘𝐽)‘{𝑦})) |
| 37 | 25, 29, 33, 35, 36 | syl22anc 839 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → ((cls‘𝐽)‘𝑢) ∈ ((nei‘𝐽)‘{𝑦})) |
| 38 | | simprrr 782 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → ((cls‘𝐽)‘𝑢) ⊆ 𝑥) |
| 39 | | vex 3484 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
| 40 | 39 | elpw2 5334 |
. . . . . . 7
⊢
(((cls‘𝐽)‘𝑢) ∈ 𝒫 𝑥 ↔ ((cls‘𝐽)‘𝑢) ⊆ 𝑥) |
| 41 | 38, 40 | sylibr 234 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → ((cls‘𝐽)‘𝑢) ∈ 𝒫 𝑥) |
| 42 | 37, 41 | elind 4200 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → ((cls‘𝐽)‘𝑢) ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)) |
| 43 | 7 | adantr 480 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → 𝐽 ∈ Comp) |
| 44 | 3 | clscld 23055 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) |
| 45 | 25, 31, 44 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) |
| 46 | | cmpcld 23410 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧
((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) → (𝐽 ↾t ((cls‘𝐽)‘𝑢)) ∈ Comp) |
| 47 | 43, 45, 46 | syl2anc 584 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → (𝐽 ↾t ((cls‘𝐽)‘𝑢)) ∈ Comp) |
| 48 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑣 = ((cls‘𝐽)‘𝑢) → (𝐽 ↾t 𝑣) = (𝐽 ↾t ((cls‘𝐽)‘𝑢))) |
| 49 | 48 | eleq1d 2826 |
. . . . . 6
⊢ (𝑣 = ((cls‘𝐽)‘𝑢) → ((𝐽 ↾t 𝑣) ∈ Comp ↔ (𝐽 ↾t ((cls‘𝐽)‘𝑢)) ∈ Comp)) |
| 50 | 49 | rspcev 3622 |
. . . . 5
⊢
((((cls‘𝐽)‘𝑢) ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝐽 ↾t ((cls‘𝐽)‘𝑢)) ∈ Comp) → ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑣) ∈ Comp) |
| 51 | 42, 47, 50 | syl2anc 584 |
. . . 4
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑢 ∈ 𝐽 ∧ (𝑦 ∈ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑥))) → ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑣) ∈ Comp) |
| 52 | 24, 51 | rexlimddv 3161 |
. . 3
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑣) ∈ Comp) |
| 53 | 52 | ralrimivva 3202 |
. 2
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) →
∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑣) ∈ Comp) |
| 54 | | isnlly 23477 |
. 2
⊢ (𝐽 ∈ 𝑛-Locally Comp
↔ (𝐽 ∈ Top ∧
∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑣) ∈ Comp)) |
| 55 | 2, 53, 54 | sylanbrc 583 |
1
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) → 𝐽 ∈ 𝑛-Locally
Comp) |