| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . . 5
⊢
(topGen‘𝐵)
∈ V |
| 2 | | eltg3 22969 |
. . . . 5
⊢
((topGen‘𝐵)
∈ V → (𝑥 ∈
(topGen‘(topGen‘𝐵)) ↔ ∃𝑦(𝑦 ⊆ (topGen‘𝐵) ∧ 𝑥 = ∪ 𝑦))) |
| 3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈
(topGen‘(topGen‘𝐵)) ↔ ∃𝑦(𝑦 ⊆ (topGen‘𝐵) ∧ 𝑥 = ∪ 𝑦)) |
| 4 | | uniiun 5058 |
. . . . . . . . . 10
⊢ ∪ 𝑦 =
∪ 𝑧 ∈ 𝑦 𝑧 |
| 5 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) → 𝑦 ⊆ (topGen‘𝐵)) |
| 6 | 5 | sselda 3983 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (topGen‘𝐵)) |
| 7 | | eltg4i 22967 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (topGen‘𝐵) → 𝑧 = ∪ (𝐵 ∩ 𝒫 𝑧)) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) ∧ 𝑧 ∈ 𝑦) → 𝑧 = ∪ (𝐵 ∩ 𝒫 𝑧)) |
| 9 | 8 | iuneq2dv 5016 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) → ∪ 𝑧 ∈ 𝑦 𝑧 = ∪ 𝑧 ∈ 𝑦 ∪ (𝐵 ∩ 𝒫 𝑧)) |
| 10 | 4, 9 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) → ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 ∪ (𝐵 ∩ 𝒫 𝑧)) |
| 11 | | iuncom4 5000 |
. . . . . . . . 9
⊢ ∪ 𝑧 ∈ 𝑦 ∪ (𝐵 ∩ 𝒫 𝑧) = ∪
∪ 𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) |
| 12 | 10, 11 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) → ∪ 𝑦 = ∪
∪ 𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧)) |
| 13 | | inss1 4237 |
. . . . . . . . . . . 12
⊢ (𝐵 ∩ 𝒫 𝑧) ⊆ 𝐵 |
| 14 | 13 | rgenw 3065 |
. . . . . . . . . . 11
⊢
∀𝑧 ∈
𝑦 (𝐵 ∩ 𝒫 𝑧) ⊆ 𝐵 |
| 15 | | iunss 5045 |
. . . . . . . . . . 11
⊢ (∪ 𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) ⊆ 𝐵 ↔ ∀𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) ⊆ 𝐵) |
| 16 | 14, 15 | mpbir 231 |
. . . . . . . . . 10
⊢ ∪ 𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) ⊆ 𝐵 |
| 17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ⊆ (topGen‘𝐵) → ∪ 𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) ⊆ 𝐵) |
| 18 | | eltg3i 22968 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ ∪
𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) ⊆ 𝐵) → ∪
∪ 𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) ∈ (topGen‘𝐵)) |
| 19 | 17, 18 | sylan2 593 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) → ∪
∪ 𝑧 ∈ 𝑦 (𝐵 ∩ 𝒫 𝑧) ∈ (topGen‘𝐵)) |
| 20 | 12, 19 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) → ∪ 𝑦 ∈ (topGen‘𝐵)) |
| 21 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑥 = ∪
𝑦 → (𝑥 ∈ (topGen‘𝐵) ↔ ∪ 𝑦
∈ (topGen‘𝐵))) |
| 22 | 20, 21 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ (topGen‘𝐵)) → (𝑥 = ∪ 𝑦 → 𝑥 ∈ (topGen‘𝐵))) |
| 23 | 22 | expimpd 453 |
. . . . 5
⊢ (𝐵 ∈ 𝑉 → ((𝑦 ⊆ (topGen‘𝐵) ∧ 𝑥 = ∪ 𝑦) → 𝑥 ∈ (topGen‘𝐵))) |
| 24 | 23 | exlimdv 1933 |
. . . 4
⊢ (𝐵 ∈ 𝑉 → (∃𝑦(𝑦 ⊆ (topGen‘𝐵) ∧ 𝑥 = ∪ 𝑦) → 𝑥 ∈ (topGen‘𝐵))) |
| 25 | 3, 24 | biimtrid 242 |
. . 3
⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ (topGen‘(topGen‘𝐵)) → 𝑥 ∈ (topGen‘𝐵))) |
| 26 | 25 | ssrdv 3989 |
. 2
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) ⊆ (topGen‘𝐵)) |
| 27 | | bastg 22973 |
. . 3
⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵)) |
| 28 | | tgss 22975 |
. . 3
⊢
(((topGen‘𝐵)
∈ V ∧ 𝐵 ⊆
(topGen‘𝐵)) →
(topGen‘𝐵) ⊆
(topGen‘(topGen‘𝐵))) |
| 29 | 1, 27, 28 | sylancr 587 |
. 2
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ⊆ (topGen‘(topGen‘𝐵))) |
| 30 | 26, 29 | eqssd 4001 |
1
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵)) |