Step | Hyp | Ref
| Expression |
1 | | rabssab 4048 |
. . . . . . 7
β’ {π¦ β Top β£ π΄ = βͺ
π¦} β {π¦ β£ π΄ = βͺ π¦} |
2 | | eqcom 2744 |
. . . . . . . 8
β’ (π΄ = βͺ
π¦ β βͺ π¦ =
π΄) |
3 | 2 | abbii 2807 |
. . . . . . 7
β’ {π¦ β£ π΄ = βͺ π¦} = {π¦ β£ βͺ π¦ = π΄} |
4 | 1, 3 | sseqtri 3985 |
. . . . . 6
β’ {π¦ β Top β£ π΄ = βͺ
π¦} β {π¦ β£ βͺ π¦ =
π΄} |
5 | | pwpwssunieq 5069 |
. . . . . 6
β’ {π¦ β£ βͺ π¦ =
π΄} β π«
π« π΄ |
6 | 4, 5 | sstri 3958 |
. . . . 5
β’ {π¦ β Top β£ π΄ = βͺ
π¦} β π«
π« π΄ |
7 | | pwexg 5338 |
. . . . . 6
β’ (π΄ β V β π« π΄ β V) |
8 | 7 | pwexd 5339 |
. . . . 5
β’ (π΄ β V β π«
π« π΄ β
V) |
9 | | ssexg 5285 |
. . . . 5
β’ (({π¦ β Top β£ π΄ = βͺ
π¦} β π«
π« π΄ β§ π«
π« π΄ β V)
β {π¦ β Top
β£ π΄ = βͺ π¦}
β V) |
10 | 6, 8, 9 | sylancr 588 |
. . . 4
β’ (π΄ β V β {π¦ β Top β£ π΄ = βͺ
π¦} β
V) |
11 | | eqeq1 2741 |
. . . . . 6
β’ (π₯ = π΄ β (π₯ = βͺ π¦ β π΄ = βͺ π¦)) |
12 | 11 | rabbidv 3418 |
. . . . 5
β’ (π₯ = π΄ β {π¦ β Top β£ π₯ = βͺ π¦} = {π¦ β Top β£ π΄ = βͺ π¦}) |
13 | | df-topon 22276 |
. . . . 5
β’ TopOn =
(π₯ β V β¦ {π¦ β Top β£ π₯ = βͺ
π¦}) |
14 | 12, 13 | fvmptg 6951 |
. . . 4
β’ ((π΄ β V β§ {π¦ β Top β£ π΄ = βͺ
π¦} β V) β
(TopOnβπ΄) = {π¦ β Top β£ π΄ = βͺ
π¦}) |
15 | 10, 14 | mpdan 686 |
. . 3
β’ (π΄ β V β
(TopOnβπ΄) = {π¦ β Top β£ π΄ = βͺ
π¦}) |
16 | 15, 6 | eqsstrdi 4003 |
. 2
β’ (π΄ β V β
(TopOnβπ΄) β
π« π« π΄) |
17 | | fvprc 6839 |
. . 3
β’ (Β¬
π΄ β V β
(TopOnβπ΄) =
β
) |
18 | | 0ss 4361 |
. . 3
β’ β
β π« π« π΄ |
19 | 17, 18 | eqsstrdi 4003 |
. 2
β’ (Β¬
π΄ β V β
(TopOnβπ΄) β
π« π« π΄) |
20 | 16, 19 | pm2.61i 182 |
1
β’
(TopOnβπ΄)
β π« π« π΄ |