Step | Hyp | Ref
| Expression |
1 | | toptopon2 20723 |
. . . . . 6
⊢ (𝑥 ∈ Top ↔ 𝑥 ∈ (TopOn‘∪ 𝑥)) |
2 | 1 | biimpi 206 |
. . . . 5
⊢ (𝑥 ∈ Top → 𝑥 ∈ (TopOn‘∪ 𝑥)) |
3 | | fvex 6201 |
. . . . . 6
⊢
(TopOn‘∪ 𝑥) ∈ V |
4 | | eleq2 2690 |
. . . . . . . 8
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (TopOn‘∪ 𝑥))) |
5 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ (𝑦 ∈ ran TopOn
↔ (TopOn‘∪ 𝑥) ∈ ran TopOn)) |
6 | 4, 5 | anbi12d 747 |
. . . . . . 7
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) ↔ (𝑥 ∈ (TopOn‘∪ 𝑥)
∧ (TopOn‘∪ 𝑥) ∈ ran TopOn))) |
7 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (TopOn‘∪ 𝑥)
∧ (TopOn‘∪ 𝑥) ∈ ran TopOn) → 𝑥 ∈ (TopOn‘∪ 𝑥)) |
8 | | fntopon 20728 |
. . . . . . . . . . . 12
⊢ TopOn Fn
V |
9 | | vuniex 6954 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥
∈ V |
10 | 8, 9 | pm3.2i 471 |
. . . . . . . . . . 11
⊢ (TopOn Fn
V ∧ ∪ 𝑥 ∈ V) |
11 | | fnfvelrn 6356 |
. . . . . . . . . . 11
⊢ ((TopOn
Fn V ∧ ∪ 𝑥 ∈ V) → (TopOn‘∪ 𝑥)
∈ ran TopOn) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
⊢
(TopOn‘∪ 𝑥) ∈ ran TopOn |
13 | 12 | jctr 565 |
. . . . . . . . 9
⊢ (𝑥 ∈ (TopOn‘∪ 𝑥)
→ (𝑥 ∈
(TopOn‘∪ 𝑥) ∧ (TopOn‘∪ 𝑥)
∈ ran TopOn)) |
14 | 7, 13 | impbii 199 |
. . . . . . . 8
⊢ ((𝑥 ∈ (TopOn‘∪ 𝑥)
∧ (TopOn‘∪ 𝑥) ∈ ran TopOn) ↔ 𝑥 ∈ (TopOn‘∪ 𝑥)) |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ ((𝑥 ∈
(TopOn‘∪ 𝑥) ∧ (TopOn‘∪ 𝑥)
∈ ran TopOn) ↔ 𝑥
∈ (TopOn‘∪ 𝑥))) |
16 | 6, 15 | bitrd 268 |
. . . . . 6
⊢ (𝑦 = (TopOn‘∪ 𝑥)
→ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) ↔ 𝑥 ∈ (TopOn‘∪ 𝑥))) |
17 | 3, 16 | spcev 3300 |
. . . . 5
⊢ (𝑥 ∈ (TopOn‘∪ 𝑥)
→ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) |
18 | 2, 17 | syl 17 |
. . . 4
⊢ (𝑥 ∈ Top → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) |
19 | | funtopon 20725 |
. . . . . . . . . 10
⊢ Fun
TopOn |
20 | | elrnrexdm 6363 |
. . . . . . . . . 10
⊢ (Fun
TopOn → (𝑦 ∈ ran
TopOn → ∃𝑧
∈ dom TopOn𝑦 =
(TopOn‘𝑧))) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran TopOn →
∃𝑧 ∈ dom
TopOn𝑦 = (TopOn‘𝑧)) |
22 | | rexex 3002 |
. . . . . . . . 9
⊢
(∃𝑧 ∈ dom
TopOn𝑦 = (TopOn‘𝑧) → ∃𝑧 𝑦 = (TopOn‘𝑧)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ ran TopOn →
∃𝑧 𝑦 = (TopOn‘𝑧)) |
24 | 23 | anim2i 593 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) → (𝑥 ∈ 𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧))) |
25 | | 19.42v 1918 |
. . . . . . . . 9
⊢
(∃𝑧(𝑥 ∈ 𝑦 ∧ 𝑦 = (TopOn‘𝑧)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧))) |
26 | 25 | biimpri 218 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧)) → ∃𝑧(𝑥 ∈ 𝑦 ∧ 𝑦 = (TopOn‘𝑧))) |
27 | | eqimss 3657 |
. . . . . . . . . . . 12
⊢ (𝑦 = (TopOn‘𝑧) → 𝑦 ⊆ (TopOn‘𝑧)) |
28 | 27 | sseld 3602 |
. . . . . . . . . . 11
⊢ (𝑦 = (TopOn‘𝑧) → (𝑥 ∈ 𝑦 → 𝑥 ∈ (TopOn‘𝑧))) |
29 | 28 | com12 32 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑦 → (𝑦 = (TopOn‘𝑧) → 𝑥 ∈ (TopOn‘𝑧))) |
30 | 29 | imp 445 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 = (TopOn‘𝑧)) → 𝑥 ∈ (TopOn‘𝑧)) |
31 | 30 | eximi 1762 |
. . . . . . . 8
⊢
(∃𝑧(𝑥 ∈ 𝑦 ∧ 𝑦 = (TopOn‘𝑧)) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧)) |
32 | 26, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑦 ∧ ∃𝑧 𝑦 = (TopOn‘𝑧)) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧)) |
33 | 24, 32 | syl 17 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) → ∃𝑧 𝑥 ∈ (TopOn‘𝑧)) |
34 | | topontop 20718 |
. . . . . . . 8
⊢ (𝑥 ∈ (TopOn‘𝑧) → 𝑥 ∈ Top) |
35 | 34 | eximi 1762 |
. . . . . . 7
⊢
(∃𝑧 𝑥 ∈ (TopOn‘𝑧) → ∃𝑧 𝑥 ∈ Top) |
36 | | ax5e 1841 |
. . . . . . 7
⊢
(∃𝑧 𝑥 ∈ Top → 𝑥 ∈ Top) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢
(∃𝑧 𝑥 ∈ (TopOn‘𝑧) → 𝑥 ∈ Top) |
38 | 33, 37 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) → 𝑥 ∈ Top) |
39 | 38 | exlimiv 1858 |
. . . 4
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) → 𝑥 ∈ Top) |
40 | 18, 39 | impbii 199 |
. . 3
⊢ (𝑥 ∈ Top ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) |
41 | | eluni 4439 |
. . . 4
⊢ (𝑥 ∈ ∪ ran TopOn ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn)) |
42 | 41 | bicomi 214 |
. . 3
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ran TopOn) ↔ 𝑥 ∈ ∪ ran
TopOn) |
43 | 40, 42 | bitri 264 |
. 2
⊢ (𝑥 ∈ Top ↔ 𝑥 ∈ ∪ ran TopOn) |
44 | 43 | eqriv 2619 |
1
⊢ Top =
∪ ran TopOn |