| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | toptopon2 22925 | . . . . 5
⊢ (𝑥 ∈ Top ↔ 𝑥 ∈ (TopOn‘∪ 𝑥)) | 
| 2 |  | fvex 6918 | . . . . . 6
⊢
(TopOn‘∪ 𝑥) ∈ V | 
| 3 |  | eleq2 2829 | . . . . . . . 8
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (TopOn‘∪ 𝑥))) | 
| 4 |  | eleq1 2828 | . . . . . . . 8
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ (𝑦 ∈ ran TopOn
↔ (TopOn‘∪ 𝑥) ∈ ran TopOn)) | 
| 5 | 3, 4 | anbi12d 632 | . . . . . . 7
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) ↔ (𝑥 ∈ (TopOn‘∪ 𝑥)
∧ (TopOn‘∪ 𝑥) ∈ ran TopOn))) | 
| 6 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑥 ∈ (TopOn‘∪ 𝑥)
∧ (TopOn‘∪ 𝑥) ∈ ran TopOn) → 𝑥 ∈ (TopOn‘∪ 𝑥)) | 
| 7 |  | fntopon 22931 | . . . . . . . . . 10
⊢ TopOn Fn
V | 
| 8 |  | vuniex 7760 | . . . . . . . . . 10
⊢ ∪ 𝑥
∈ V | 
| 9 |  | fnfvelrn 7099 | . . . . . . . . . 10
⊢ ((TopOn
Fn V ∧ ∪ 𝑥 ∈ V) → (TopOn‘∪ 𝑥)
∈ ran TopOn) | 
| 10 | 7, 8, 9 | mp2an 692 | . . . . . . . . 9
⊢
(TopOn‘∪ 𝑥) ∈ ran TopOn | 
| 11 | 10 | jctr 524 | . . . . . . . 8
⊢ (𝑥 ∈ (TopOn‘∪ 𝑥)
→ (𝑥 ∈
(TopOn‘∪ 𝑥) ∧ (TopOn‘∪ 𝑥)
∈ ran TopOn)) | 
| 12 | 6, 11 | impbii 209 | . . . . . . 7
⊢ ((𝑥 ∈ (TopOn‘∪ 𝑥)
∧ (TopOn‘∪ 𝑥) ∈ ran TopOn) ↔ 𝑥 ∈ (TopOn‘∪ 𝑥)) | 
| 13 | 5, 12 | bitrdi 287 | . . . . . 6
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) ↔ 𝑥 ∈ (TopOn‘∪ 𝑥))) | 
| 14 | 2, 13 | spcev 3605 | . . . . 5
⊢ (𝑥 ∈ (TopOn‘∪ 𝑥)
→ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) | 
| 15 | 1, 14 | sylbi 217 | . . . 4
⊢ (𝑥 ∈ Top → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) | 
| 16 |  | funtopon 22927 | . . . . . . . . 9
⊢ Fun
TopOn | 
| 17 |  | elrnrexdm 7108 | . . . . . . . . 9
⊢ (Fun
TopOn → (𝑦 ∈ ran
TopOn → ∃𝑧
∈ dom TopOn𝑦 =
(TopOn‘𝑧))) | 
| 18 | 16, 17 | ax-mp 5 | . . . . . . . 8
⊢ (𝑦 ∈ ran TopOn →
∃𝑧 ∈ dom
TopOn𝑦 = (TopOn‘𝑧)) | 
| 19 |  | rexex 3075 | . . . . . . . 8
⊢
(∃𝑧 ∈ dom
TopOn𝑦 = (TopOn‘𝑧) → ∃𝑧 𝑦 = (TopOn‘𝑧)) | 
| 20 | 18, 19 | syl 17 | . . . . . . 7
⊢ (𝑦 ∈ ran TopOn →
∃𝑧 𝑦 = (TopOn‘𝑧)) | 
| 21 |  | 19.42v 1952 | . . . . . . . 8
⊢
(∃𝑧(𝑥 ∈ 𝑦 ∧ 𝑦 = (TopOn‘𝑧)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧))) | 
| 22 |  | eqimss 4041 | . . . . . . . . . . 11
⊢ (𝑦 = (TopOn‘𝑧) → 𝑦 ⊆ (TopOn‘𝑧)) | 
| 23 | 22 | sseld 3981 | . . . . . . . . . 10
⊢ (𝑦 = (TopOn‘𝑧) → (𝑥 ∈ 𝑦 → 𝑥 ∈ (TopOn‘𝑧))) | 
| 24 | 23 | impcom 407 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 = (TopOn‘𝑧)) → 𝑥 ∈ (TopOn‘𝑧)) | 
| 25 | 24 | eximi 1834 | . . . . . . . 8
⊢
(∃𝑧(𝑥 ∈ 𝑦 ∧ 𝑦 = (TopOn‘𝑧)) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧)) | 
| 26 | 21, 25 | sylbir 235 | . . . . . . 7
⊢ ((𝑥 ∈ 𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧)) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧)) | 
| 27 | 20, 26 | sylan2 593 | . . . . . 6
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧)) | 
| 28 |  | topontop 22920 | . . . . . . 7
⊢ (𝑥 ∈ (TopOn‘𝑧) → 𝑥 ∈ Top) | 
| 29 | 28 | exlimiv 1929 | . . . . . 6
⊢
(∃𝑧 𝑥 ∈ (TopOn‘𝑧) → 𝑥 ∈ Top) | 
| 30 | 27, 29 | syl 17 | . . . . 5
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) → 𝑥 ∈ Top) | 
| 31 | 30 | exlimiv 1929 | . . . 4
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) → 𝑥 ∈ Top) | 
| 32 | 15, 31 | impbii 209 | . . 3
⊢ (𝑥 ∈ Top ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) | 
| 33 |  | eluni 4909 | . . 3
⊢ (𝑥 ∈ ∪ ran TopOn ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) | 
| 34 | 32, 33 | bitr4i 278 | . 2
⊢ (𝑥 ∈ Top ↔ 𝑥 ∈ ∪ ran TopOn) | 
| 35 | 34 | eqriv 2733 | 1
⊢ Top =
∪ ran TopOn |