Step | Hyp | Ref
| Expression |
1 | | toptopon2 22290 |
. . . . 5
β’ (π₯ β Top β π₯ β (TopOnββͺ π₯)) |
2 | | fvex 6859 |
. . . . . 6
β’
(TopOnββͺ π₯) β V |
3 | | eleq2 2823 |
. . . . . . . 8
β’ (π¦ = (TopOnββͺ π₯)
β (π₯ β π¦ β π₯ β (TopOnββͺ π₯))) |
4 | | eleq1 2822 |
. . . . . . . 8
β’ (π¦ = (TopOnββͺ π₯)
β (π¦ β ran TopOn
β (TopOnββͺ π₯) β ran TopOn)) |
5 | 3, 4 | anbi12d 632 |
. . . . . . 7
β’ (π¦ = (TopOnββͺ π₯)
β ((π₯ β π¦ β§ π¦ β ran TopOn) β (π₯ β (TopOnββͺ π₯)
β§ (TopOnββͺ π₯) β ran TopOn))) |
6 | | simpl 484 |
. . . . . . . 8
β’ ((π₯ β (TopOnββͺ π₯)
β§ (TopOnββͺ π₯) β ran TopOn) β π₯ β (TopOnββͺ π₯)) |
7 | | fntopon 22296 |
. . . . . . . . . 10
β’ TopOn Fn
V |
8 | | vuniex 7680 |
. . . . . . . . . 10
β’ βͺ π₯
β V |
9 | | fnfvelrn 7035 |
. . . . . . . . . 10
β’ ((TopOn
Fn V β§ βͺ π₯ β V) β (TopOnββͺ π₯)
β ran TopOn) |
10 | 7, 8, 9 | mp2an 691 |
. . . . . . . . 9
β’
(TopOnββͺ π₯) β ran TopOn |
11 | 10 | jctr 526 |
. . . . . . . 8
β’ (π₯ β (TopOnββͺ π₯)
β (π₯ β
(TopOnββͺ π₯) β§ (TopOnββͺ π₯)
β ran TopOn)) |
12 | 6, 11 | impbii 208 |
. . . . . . 7
β’ ((π₯ β (TopOnββͺ π₯)
β§ (TopOnββͺ π₯) β ran TopOn) β π₯ β (TopOnββͺ π₯)) |
13 | 5, 12 | bitrdi 287 |
. . . . . 6
β’ (π¦ = (TopOnββͺ π₯)
β ((π₯ β π¦ β§ π¦ β ran TopOn) β π₯ β (TopOnββͺ π₯))) |
14 | 2, 13 | spcev 3567 |
. . . . 5
β’ (π₯ β (TopOnββͺ π₯)
β βπ¦(π₯ β π¦ β§ π¦ β ran TopOn)) |
15 | 1, 14 | sylbi 216 |
. . . 4
β’ (π₯ β Top β βπ¦(π₯ β π¦ β§ π¦ β ran TopOn)) |
16 | | funtopon 22292 |
. . . . . . . . 9
β’ Fun
TopOn |
17 | | elrnrexdm 7043 |
. . . . . . . . 9
β’ (Fun
TopOn β (π¦ β ran
TopOn β βπ§
β dom TopOnπ¦ =
(TopOnβπ§))) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
β’ (π¦ β ran TopOn β
βπ§ β dom
TopOnπ¦ = (TopOnβπ§)) |
19 | | rexex 3076 |
. . . . . . . 8
β’
(βπ§ β dom
TopOnπ¦ = (TopOnβπ§) β βπ§ π¦ = (TopOnβπ§)) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (π¦ β ran TopOn β
βπ§ π¦ = (TopOnβπ§)) |
21 | | 19.42v 1958 |
. . . . . . . 8
β’
(βπ§(π₯ β π¦ β§ π¦ = (TopOnβπ§)) β (π₯ β π¦ β§ βπ§ π¦ = (TopOnβπ§))) |
22 | | eqimss 4004 |
. . . . . . . . . . 11
β’ (π¦ = (TopOnβπ§) β π¦ β (TopOnβπ§)) |
23 | 22 | sseld 3947 |
. . . . . . . . . 10
β’ (π¦ = (TopOnβπ§) β (π₯ β π¦ β π₯ β (TopOnβπ§))) |
24 | 23 | impcom 409 |
. . . . . . . . 9
β’ ((π₯ β π¦ β§ π¦ = (TopOnβπ§)) β π₯ β (TopOnβπ§)) |
25 | 24 | eximi 1838 |
. . . . . . . 8
β’
(βπ§(π₯ β π¦ β§ π¦ = (TopOnβπ§)) β βπ§ π₯ β (TopOnβπ§)) |
26 | 21, 25 | sylbir 234 |
. . . . . . 7
β’ ((π₯ β π¦ β§ βπ§ π¦ = (TopOnβπ§)) β βπ§ π₯ β (TopOnβπ§)) |
27 | 20, 26 | sylan2 594 |
. . . . . 6
β’ ((π₯ β π¦ β§ π¦ β ran TopOn) β βπ§ π₯ β (TopOnβπ§)) |
28 | | topontop 22285 |
. . . . . . 7
β’ (π₯ β (TopOnβπ§) β π₯ β Top) |
29 | 28 | exlimiv 1934 |
. . . . . 6
β’
(βπ§ π₯ β (TopOnβπ§) β π₯ β Top) |
30 | 27, 29 | syl 17 |
. . . . 5
β’ ((π₯ β π¦ β§ π¦ β ran TopOn) β π₯ β Top) |
31 | 30 | exlimiv 1934 |
. . . 4
β’
(βπ¦(π₯ β π¦ β§ π¦ β ran TopOn) β π₯ β Top) |
32 | 15, 31 | impbii 208 |
. . 3
β’ (π₯ β Top β βπ¦(π₯ β π¦ β§ π¦ β ran TopOn)) |
33 | | eluni 4872 |
. . 3
β’ (π₯ β βͺ ran TopOn β βπ¦(π₯ β π¦ β§ π¦ β ran TopOn)) |
34 | 32, 33 | bitr4i 278 |
. 2
β’ (π₯ β Top β π₯ β βͺ ran TopOn) |
35 | 34 | eqriv 2730 |
1
β’ Top =
βͺ ran TopOn |