| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eltg4i 22968 | . . . . . 6
⊢ (𝑥 ∈ (topGen‘𝐵) → 𝑥 = ∪ (𝐵 ∩ 𝒫 𝑥)) | 
| 2 |  | inex1g 5318 | . . . . . . 7
⊢ (𝐵 ∈ On → (𝐵 ∩ 𝒫 𝑥) ∈ V) | 
| 3 |  | onss 7806 | . . . . . . . 8
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) | 
| 4 |  | ssinss1 4245 | . . . . . . . 8
⊢ (𝐵 ⊆ On → (𝐵 ∩ 𝒫 𝑥) ⊆ On) | 
| 5 | 3, 4 | syl 17 | . . . . . . 7
⊢ (𝐵 ∈ On → (𝐵 ∩ 𝒫 𝑥) ⊆ On) | 
| 6 |  | ssonuni 7801 | . . . . . . 7
⊢ ((𝐵 ∩ 𝒫 𝑥) ∈ V → ((𝐵 ∩ 𝒫 𝑥) ⊆ On → ∪ (𝐵
∩ 𝒫 𝑥) ∈
On)) | 
| 7 | 2, 5, 6 | sylc 65 | . . . . . 6
⊢ (𝐵 ∈ On → ∪ (𝐵
∩ 𝒫 𝑥) ∈
On) | 
| 8 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑥 = ∪
(𝐵 ∩ 𝒫 𝑥) → (𝑥 ∈ On ↔ ∪ (𝐵
∩ 𝒫 𝑥) ∈
On)) | 
| 9 | 8 | biimprd 248 | . . . . . 6
⊢ (𝑥 = ∪
(𝐵 ∩ 𝒫 𝑥) → (∪ (𝐵
∩ 𝒫 𝑥) ∈
On → 𝑥 ∈
On)) | 
| 10 | 1, 7, 9 | syl2imc 41 | . . . . 5
⊢ (𝐵 ∈ On → (𝑥 ∈ (topGen‘𝐵) → 𝑥 ∈ On)) | 
| 11 |  | onuni 7809 | . . . . . 6
⊢ (𝐵 ∈ On → ∪ 𝐵
∈ On) | 
| 12 |  | onsuc 7832 | . . . . . 6
⊢ (∪ 𝐵
∈ On → suc ∪ 𝐵 ∈ On) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ (𝐵 ∈ On → suc ∪ 𝐵
∈ On) | 
| 14 | 10, 13 | jctird 526 | . . . 4
⊢ (𝐵 ∈ On → (𝑥 ∈ (topGen‘𝐵) → (𝑥 ∈ On ∧ suc ∪ 𝐵
∈ On))) | 
| 15 |  | tg1 22972 | . . . . . 6
⊢ (𝑥 ∈ (topGen‘𝐵) → 𝑥 ⊆ ∪ 𝐵) | 
| 16 | 15 | a1i 11 | . . . . 5
⊢ (𝐵 ∈ On → (𝑥 ∈ (topGen‘𝐵) → 𝑥 ⊆ ∪ 𝐵)) | 
| 17 |  | sucidg 6464 | . . . . . 6
⊢ (∪ 𝐵
∈ On → ∪ 𝐵 ∈ suc ∪
𝐵) | 
| 18 | 11, 17 | syl 17 | . . . . 5
⊢ (𝐵 ∈ On → ∪ 𝐵
∈ suc ∪ 𝐵) | 
| 19 | 16, 18 | jctird 526 | . . . 4
⊢ (𝐵 ∈ On → (𝑥 ∈ (topGen‘𝐵) → (𝑥 ⊆ ∪ 𝐵 ∧ ∪ 𝐵
∈ suc ∪ 𝐵))) | 
| 20 |  | ontr2 6430 | . . . 4
⊢ ((𝑥 ∈ On ∧ suc ∪ 𝐵
∈ On) → ((𝑥
⊆ ∪ 𝐵 ∧ ∪ 𝐵 ∈ suc ∪ 𝐵)
→ 𝑥 ∈ suc ∪ 𝐵)) | 
| 21 | 14, 19, 20 | syl6c 70 | . . 3
⊢ (𝐵 ∈ On → (𝑥 ∈ (topGen‘𝐵) → 𝑥 ∈ suc ∪
𝐵)) | 
| 22 |  | elsuci 6450 | . . . 4
⊢ (𝑥 ∈ suc ∪ 𝐵
→ (𝑥 ∈ ∪ 𝐵
∨ 𝑥 = ∪ 𝐵)) | 
| 23 |  | eloni 6393 | . . . . . . . 8
⊢ (𝐵 ∈ On → Ord 𝐵) | 
| 24 |  | orduniss 6480 | . . . . . . . 8
⊢ (Ord
𝐵 → ∪ 𝐵
⊆ 𝐵) | 
| 25 | 23, 24 | syl 17 | . . . . . . 7
⊢ (𝐵 ∈ On → ∪ 𝐵
⊆ 𝐵) | 
| 26 |  | bastg 22974 | . . . . . . 7
⊢ (𝐵 ∈ On → 𝐵 ⊆ (topGen‘𝐵)) | 
| 27 | 25, 26 | sstrd 3993 | . . . . . 6
⊢ (𝐵 ∈ On → ∪ 𝐵
⊆ (topGen‘𝐵)) | 
| 28 | 27 | sseld 3981 | . . . . 5
⊢ (𝐵 ∈ On → (𝑥 ∈ ∪ 𝐵
→ 𝑥 ∈
(topGen‘𝐵))) | 
| 29 |  | ssid 4005 | . . . . . . 7
⊢ 𝐵 ⊆ 𝐵 | 
| 30 |  | eltg3i 22969 | . . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐵 ⊆ 𝐵) → ∪ 𝐵 ∈ (topGen‘𝐵)) | 
| 31 | 29, 30 | mpan2 691 | . . . . . 6
⊢ (𝐵 ∈ On → ∪ 𝐵
∈ (topGen‘𝐵)) | 
| 32 |  | eleq1a 2835 | . . . . . 6
⊢ (∪ 𝐵
∈ (topGen‘𝐵)
→ (𝑥 = ∪ 𝐵
→ 𝑥 ∈
(topGen‘𝐵))) | 
| 33 | 31, 32 | syl 17 | . . . . 5
⊢ (𝐵 ∈ On → (𝑥 = ∪
𝐵 → 𝑥 ∈ (topGen‘𝐵))) | 
| 34 | 28, 33 | jaod 859 | . . . 4
⊢ (𝐵 ∈ On → ((𝑥 ∈ ∪ 𝐵
∨ 𝑥 = ∪ 𝐵)
→ 𝑥 ∈
(topGen‘𝐵))) | 
| 35 | 22, 34 | syl5 34 | . . 3
⊢ (𝐵 ∈ On → (𝑥 ∈ suc ∪ 𝐵
→ 𝑥 ∈
(topGen‘𝐵))) | 
| 36 | 21, 35 | impbid 212 | . 2
⊢ (𝐵 ∈ On → (𝑥 ∈ (topGen‘𝐵) ↔ 𝑥 ∈ suc ∪
𝐵)) | 
| 37 | 36 | eqrdv 2734 | 1
⊢ (𝐵 ∈ On →
(topGen‘𝐵) = suc
∪ 𝐵) |