| Step | Hyp | Ref
| Expression |
| 1 | | topgele 22936 |
. . . 4
⊢ (𝐵 ∈ (TopOn‘𝐴) → ({∅, 𝐴} ⊆ 𝐵 ∧ 𝐵 ⊆ 𝒫 𝐴)) |
| 2 | 1 | adantl 481 |
. . 3
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → ({∅, 𝐴} ⊆ 𝐵 ∧ 𝐵 ⊆ 𝒫 𝐴)) |
| 3 | 2 | simprd 495 |
. 2
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 ⊆ 𝒫 𝐴) |
| 4 | | velpw 4605 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| 5 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 ∈ (TopOn‘𝐴)) |
| 6 | | df-ima 5698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ 𝐴 ↦ {𝑧}) “ 𝑥) = ran ((𝑧 ∈ 𝐴 ↦ {𝑧}) ↾ 𝑥) |
| 7 | | resmpt 6055 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ⊆ 𝐴 → ((𝑧 ∈ 𝐴 ↦ {𝑧}) ↾ 𝑥) = (𝑧 ∈ 𝑥 ↦ {𝑧})) |
| 8 | 7 | rneqd 5949 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ⊆ 𝐴 → ran ((𝑧 ∈ 𝐴 ↦ {𝑧}) ↾ 𝑥) = ran (𝑧 ∈ 𝑥 ↦ {𝑧})) |
| 9 | 6, 8 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ⊆ 𝐴 → ((𝑧 ∈ 𝐴 ↦ {𝑧}) “ 𝑥) = ran (𝑧 ∈ 𝑥 ↦ {𝑧})) |
| 10 | | rnmptsn 37336 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(𝑧 ∈ 𝑥 ↦ {𝑧}) = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} |
| 11 | 9, 10 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ 𝐴 → ((𝑧 ∈ 𝐴 ↦ {𝑧}) “ 𝑥) = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}) |
| 12 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝐴 ↦ {𝑧}) “ 𝑥) ⊆ ran (𝑧 ∈ 𝐴 ↦ {𝑧}) |
| 13 | 11, 12 | eqsstrrdi 4029 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ 𝐴 → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ ran (𝑧 ∈ 𝐴 ↦ {𝑧})) |
| 14 | | rnmptsn 37336 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑧 ∈ 𝐴 ↦ {𝑧}) = {𝑢 ∣ ∃𝑧 ∈ 𝐴 𝑢 = {𝑧}} |
| 15 | 13, 14 | sseqtrdi 4024 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝐴 → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ {𝑢 ∣ ∃𝑧 ∈ 𝐴 𝑢 = {𝑧}}) |
| 16 | | dissneq.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} |
| 17 | | sneq 4636 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
| 18 | 17 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝑢 = {𝑥} ↔ 𝑢 = {𝑧})) |
| 19 | 18 | cbvrexvw 3238 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥 ∈
𝐴 𝑢 = {𝑥} ↔ ∃𝑧 ∈ 𝐴 𝑢 = {𝑧}) |
| 20 | 19 | abbii 2809 |
. . . . . . . . . . . . . . 15
⊢ {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} = {𝑢 ∣ ∃𝑧 ∈ 𝐴 𝑢 = {𝑧}} |
| 21 | 16, 20 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ 𝐶 = {𝑢 ∣ ∃𝑧 ∈ 𝐴 𝑢 = {𝑧}} |
| 22 | 15, 21 | sseqtrrdi 4025 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ 𝐴 → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐶) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐶) |
| 24 | | sstr 3992 |
. . . . . . . . . . . . . 14
⊢ (({𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵) |
| 25 | 24 | expcom 413 |
. . . . . . . . . . . . 13
⊢ (𝐶 ⊆ 𝐵 → ({𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐶 → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵)) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → ({𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐶 → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵)) |
| 27 | 23, 26 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵) |
| 28 | 27 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ∧ 𝐵 ∈ (TopOn‘𝐴)) → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵) |
| 29 | 5, 28 | ssexd 5324 |
. . . . . . . . 9
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ∧ 𝐵 ∈ (TopOn‘𝐴)) → {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ∈ V) |
| 30 | | isset 3494 |
. . . . . . . . 9
⊢ ({𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ∈ V ↔ ∃𝑦 𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}) |
| 31 | 29, 30 | sylib 218 |
. . . . . . . 8
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ∧ 𝐵 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝐴 ↦ {𝑧}) = (𝑧 ∈ 𝐴 ↦ {𝑧}) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ {𝑢 ∣ ∃𝑧 ∈ 𝐴 𝑢 = {𝑧}} = {𝑢 ∣ ∃𝑧 ∈ 𝐴 𝑢 = {𝑧}} |
| 34 | 32, 33 | mptsnun 37340 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝐴 → 𝑥 = ∪ ((𝑧 ∈ 𝐴 ↦ {𝑧}) “ 𝑥)) |
| 35 | 11 | unieqd 4920 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝐴 → ∪ ((𝑧 ∈ 𝐴 ↦ {𝑧}) “ 𝑥) = ∪ {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}) |
| 36 | 34, 35 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ 𝐴 → 𝑥 = ∪ {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 = ∪ {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}) |
| 38 | 27, 37 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → ({𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵 ∧ 𝑥 = ∪ {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}})) |
| 39 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} → (𝑦 ⊆ 𝐵 ↔ {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵)) |
| 40 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} → ∪ 𝑦 = ∪
{𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}) |
| 41 | 40 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} → (𝑥 = ∪ 𝑦 ↔ 𝑥 = ∪ {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}})) |
| 42 | 39, 41 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} → ((𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦) ↔ ({𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} ⊆ 𝐵 ∧ 𝑥 = ∪ {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}}))) |
| 43 | 38, 42 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → (𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} → (𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
| 44 | 43 | eximdv 1917 |
. . . . . . . . 9
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} → ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
| 45 | 44 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ∧ 𝐵 ∈ (TopOn‘𝐴)) → (∃𝑦 𝑦 = {𝑢 ∣ ∃𝑧 ∈ 𝑥 𝑢 = {𝑧}} → ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
| 46 | 31, 45 | mpd 15 |
. . . . . . 7
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ∧ 𝐵 ∈ (TopOn‘𝐴)) → ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)) |
| 47 | 4, 46 | syl3an2b 1406 |
. . . . . 6
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ∧ 𝐵 ∈ (TopOn‘𝐴)) → ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)) |
| 48 | 47 | 3com23 1127 |
. . . . 5
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴) ∧ 𝑥 ∈ 𝒫 𝐴) → ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)) |
| 49 | 48 | 3expia 1122 |
. . . 4
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → (𝑥 ∈ 𝒫 𝐴 → ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
| 50 | | topontop 22919 |
. . . . . . . 8
⊢ (𝐵 ∈ (TopOn‘𝐴) → 𝐵 ∈ Top) |
| 51 | | tgtop 22980 |
. . . . . . . 8
⊢ (𝐵 ∈ Top →
(topGen‘𝐵) = 𝐵) |
| 52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ (TopOn‘𝐴) → (topGen‘𝐵) = 𝐵) |
| 53 | 52 | eleq2d 2827 |
. . . . . 6
⊢ (𝐵 ∈ (TopOn‘𝐴) → (𝑥 ∈ (topGen‘𝐵) ↔ 𝑥 ∈ 𝐵)) |
| 54 | | eltg3 22969 |
. . . . . 6
⊢ (𝐵 ∈ (TopOn‘𝐴) → (𝑥 ∈ (topGen‘𝐵) ↔ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
| 55 | 53, 54 | bitr3d 281 |
. . . . 5
⊢ (𝐵 ∈ (TopOn‘𝐴) → (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
| 56 | 55 | adantl 481 |
. . . 4
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
| 57 | 49, 56 | sylibrd 259 |
. . 3
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝐵)) |
| 58 | 57 | ssrdv 3989 |
. 2
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝒫 𝐴 ⊆ 𝐵) |
| 59 | 3, 58 | eqssd 4001 |
1
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴) |