Step | Hyp | Ref
| Expression |
1 | | elex 2750 |
. . 3
β’ (π΄ β π β π΄ β V) |
2 | | rabssab 3245 |
. . . . . 6
β’ {π¦ β Top β£ π΄ = βͺ
π¦} β {π¦ β£ π΄ = βͺ π¦} |
3 | | eqcom 2179 |
. . . . . . 7
β’ (π΄ = βͺ
π¦ β βͺ π¦ =
π΄) |
4 | 3 | abbii 2293 |
. . . . . 6
β’ {π¦ β£ π΄ = βͺ π¦} = {π¦ β£ βͺ π¦ = π΄} |
5 | 2, 4 | sseqtri 3191 |
. . . . 5
β’ {π¦ β Top β£ π΄ = βͺ
π¦} β {π¦ β£ βͺ π¦ =
π΄} |
6 | | pwpwssunieq 3977 |
. . . . 5
β’ {π¦ β£ βͺ π¦ =
π΄} β π«
π« π΄ |
7 | 5, 6 | sstri 3166 |
. . . 4
β’ {π¦ β Top β£ π΄ = βͺ
π¦} β π«
π« π΄ |
8 | | pwexg 4182 |
. . . . 5
β’ (π΄ β π β π« π΄ β V) |
9 | 8 | pwexd 4183 |
. . . 4
β’ (π΄ β π β π« π« π΄ β V) |
10 | | ssexg 4144 |
. . . 4
β’ (({π¦ β Top β£ π΄ = βͺ
π¦} β π«
π« π΄ β§ π«
π« π΄ β V)
β {π¦ β Top
β£ π΄ = βͺ π¦}
β V) |
11 | 7, 9, 10 | sylancr 414 |
. . 3
β’ (π΄ β π β {π¦ β Top β£ π΄ = βͺ π¦} β V) |
12 | | eqeq1 2184 |
. . . . 5
β’ (π₯ = π΄ β (π₯ = βͺ π¦ β π΄ = βͺ π¦)) |
13 | 12 | rabbidv 2728 |
. . . 4
β’ (π₯ = π΄ β {π¦ β Top β£ π₯ = βͺ π¦} = {π¦ β Top β£ π΄ = βͺ π¦}) |
14 | | df-topon 13596 |
. . . 4
β’ TopOn =
(π₯ β V β¦ {π¦ β Top β£ π₯ = βͺ
π¦}) |
15 | 13, 14 | fvmptg 5594 |
. . 3
β’ ((π΄ β V β§ {π¦ β Top β£ π΄ = βͺ
π¦} β V) β
(TopOnβπ΄) = {π¦ β Top β£ π΄ = βͺ
π¦}) |
16 | 1, 11, 15 | syl2anc 411 |
. 2
β’ (π΄ β π β (TopOnβπ΄) = {π¦ β Top β£ π΄ = βͺ π¦}) |
17 | 16, 7 | eqsstrdi 3209 |
1
β’ (π΄ β π β (TopOnβπ΄) β π« π« π΄) |