Proof of Theorem neiptopreu
| Step | Hyp | Ref
| Expression |
| 1 | | neiptop.o |
. . . . 5
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} |
| 2 | | neiptop.0 |
. . . . 5
⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) |
| 3 | | neiptop.1 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) |
| 4 | | neiptop.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |
| 5 | | neiptop.3 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) |
| 6 | | neiptop.4 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) |
| 7 | | neiptop.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | neiptoptop 23139 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Top) |
| 9 | | toptopon2 22924 |
. . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 10 | 8, 9 | sylib 218 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 11 | 1, 2, 3, 4, 5, 6, 7 | neiptopuni 23138 |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 12 | 11 | fveq2d 6910 |
. . 3
⊢ (𝜑 → (TopOn‘𝑋) = (TopOn‘∪ 𝐽)) |
| 13 | 10, 12 | eleqtrrd 2844 |
. 2
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 14 | 1, 2, 3, 4, 5, 6, 7 | neiptopnei 23140 |
. 2
⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝}))) |
| 15 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑝(𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) |
| 16 | | nfmpt1 5250 |
. . . . . . . . . . 11
⊢
Ⅎ𝑝(𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) |
| 17 | 16 | nfeq2 2923 |
. . . . . . . . . 10
⊢
Ⅎ𝑝 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) |
| 18 | 15, 17 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑝((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) |
| 19 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑝 𝑏 ⊆ 𝑋 |
| 20 | 18, 19 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑝(((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) |
| 21 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) ∧ 𝑝 ∈ 𝑏) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) |
| 22 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) → 𝑏 ⊆ 𝑋) |
| 23 | 22 | sselda 3983 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) ∧ 𝑝 ∈ 𝑏) → 𝑝 ∈ 𝑋) |
| 24 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) |
| 25 | | fvexd 6921 |
. . . . . . . . . . . 12
⊢ ((𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) ∧ 𝑝 ∈ 𝑋) → ((nei‘𝑗)‘{𝑝}) ∈ V) |
| 26 | 24, 25 | fvmpt2d 7029 |
. . . . . . . . . . 11
⊢ ((𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ((nei‘𝑗)‘{𝑝})) |
| 27 | 21, 23, 26 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) ∧ 𝑝 ∈ 𝑏) → (𝑁‘𝑝) = ((nei‘𝑗)‘{𝑝})) |
| 28 | 27 | eqcomd 2743 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) ∧ 𝑝 ∈ 𝑏) → ((nei‘𝑗)‘{𝑝}) = (𝑁‘𝑝)) |
| 29 | 28 | eleq2d 2827 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) ∧ 𝑝 ∈ 𝑏) → (𝑏 ∈ ((nei‘𝑗)‘{𝑝}) ↔ 𝑏 ∈ (𝑁‘𝑝))) |
| 30 | 20, 29 | ralbida 3270 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ⊆ 𝑋) → (∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝}) ↔ ∀𝑝 ∈ 𝑏 𝑏 ∈ (𝑁‘𝑝))) |
| 31 | 30 | pm5.32da 579 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) → ((𝑏 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝})) ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ (𝑁‘𝑝)))) |
| 32 | | toponss 22933 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (TopOn‘𝑋) ∧ 𝑏 ∈ 𝑗) → 𝑏 ⊆ 𝑋) |
| 33 | 32 | ad4ant24 754 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ∈ 𝑗) → 𝑏 ⊆ 𝑋) |
| 34 | | topontop 22919 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (TopOn‘𝑋) → 𝑗 ∈ Top) |
| 35 | 34 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) → 𝑗 ∈ Top) |
| 36 | | opnnei 23128 |
. . . . . . . . . 10
⊢ (𝑗 ∈ Top → (𝑏 ∈ 𝑗 ↔ ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝}))) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) → (𝑏 ∈ 𝑗 ↔ ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝}))) |
| 38 | 37 | biimpa 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ∈ 𝑗) → ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝})) |
| 39 | 33, 38 | jca 511 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ 𝑏 ∈ 𝑗) → (𝑏 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝}))) |
| 40 | 37 | biimpar 477 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝})) → 𝑏 ∈ 𝑗) |
| 41 | 40 | adantrl 716 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) ∧ (𝑏 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝}))) → 𝑏 ∈ 𝑗) |
| 42 | 39, 41 | impbida 801 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) → (𝑏 ∈ 𝑗 ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ ((nei‘𝑗)‘{𝑝})))) |
| 43 | 1 | neipeltop 23137 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐽 ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ (𝑁‘𝑝))) |
| 44 | 43 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) → (𝑏 ∈ 𝐽 ↔ (𝑏 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑏 𝑏 ∈ (𝑁‘𝑝)))) |
| 45 | 31, 42, 44 | 3bitr4d 311 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) → (𝑏 ∈ 𝑗 ↔ 𝑏 ∈ 𝐽)) |
| 46 | 45 | eqrdv 2735 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) → 𝑗 = 𝐽) |
| 47 | 46 | ex 412 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (TopOn‘𝑋)) → (𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) → 𝑗 = 𝐽)) |
| 48 | 47 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑗 ∈ (TopOn‘𝑋)(𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) → 𝑗 = 𝐽)) |
| 49 | | simpl 482 |
. . . . . . 7
⊢ ((𝑗 = 𝐽 ∧ 𝑝 ∈ 𝑋) → 𝑗 = 𝐽) |
| 50 | 49 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑗 = 𝐽 ∧ 𝑝 ∈ 𝑋) → (nei‘𝑗) = (nei‘𝐽)) |
| 51 | 50 | fveq1d 6908 |
. . . . 5
⊢ ((𝑗 = 𝐽 ∧ 𝑝 ∈ 𝑋) → ((nei‘𝑗)‘{𝑝}) = ((nei‘𝐽)‘{𝑝})) |
| 52 | 51 | mpteq2dva 5242 |
. . . 4
⊢ (𝑗 = 𝐽 → (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝}))) |
| 53 | 52 | eqeq2d 2748 |
. . 3
⊢ (𝑗 = 𝐽 → (𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) ↔ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))) |
| 54 | 53 | eqreu 3735 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})) ∧ ∀𝑗 ∈ (TopOn‘𝑋)(𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})) → 𝑗 = 𝐽)) → ∃!𝑗 ∈ (TopOn‘𝑋)𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) |
| 55 | 13, 14, 48, 54 | syl3anc 1373 |
1
⊢ (𝜑 → ∃!𝑗 ∈ (TopOn‘𝑋)𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) |