| Step | Hyp | Ref
| Expression |
|---|
| 1 | | elfvex 6930 |
. 2
β’ (π½ β (TopOnβπ΅) β π΅ β V) |
| 2 | | uniexg 7730 |
. . . 4
β’ (π½ β Top β βͺ π½
β V) |
| 3 | | eleq1 2822 |
. . . 4
β’ (π΅ = βͺ
π½ β (π΅ β V β βͺ π½
β V)) |
| 4 | 2, 3 | syl5ibrcom 246 |
. . 3
β’ (π½ β Top β (π΅ = βͺ
π½ β π΅ β V)) |
| 5 | 4 | imp 408 |
. 2
β’ ((π½ β Top β§ π΅ = βͺ
π½) β π΅ β V) |
| 6 | | eqeq1 2737 |
. . . . . 6
β’ (π = π΅ β (π = βͺ π β π΅ = βͺ π)) |
| 7 | 6 | rabbidv 3441 |
. . . . 5
β’ (π = π΅ β {π β Top β£ π = βͺ π} = {π β Top β£ π΅ = βͺ π}) |
| 8 | | df-topon 22413 |
. . . . 5
β’ TopOn =
(π β V β¦ {π β Top β£ π = βͺ
π}) |
| 9 | | vpwex 5376 |
. . . . . . 7
β’ π«
π β V |
| 10 | 9 | pwex 5379 |
. . . . . 6
β’ π«
π« π β
V |
| 11 | | rabss 4070 |
. . . . . . 7
β’ ({π β Top β£ π = βͺ
π} β π«
π« π β
βπ β Top (π = βͺ
π β π β π« π« π)) |
| 12 | | pwuni 4950 |
. . . . . . . . . 10
β’ π β π« βͺ π |
| 13 | | pweq 4617 |
. . . . . . . . . 10
β’ (π = βͺ
π β π« π = π« βͺ π) |
| 14 | 12, 13 | sseqtrrid 4036 |
. . . . . . . . 9
β’ (π = βͺ
π β π β π« π) |
| 15 | | velpw 4608 |
. . . . . . . . 9
β’ (π β π« π«
π β π β π« π) |
| 16 | 14, 15 | sylibr 233 |
. . . . . . . 8
β’ (π = βͺ
π β π β π« π« π) |
| 17 | 16 | a1i 11 |
. . . . . . 7
β’ (π β Top β (π = βͺ
π β π β π« π« π)) |
| 18 | 11, 17 | mprgbir 3069 |
. . . . . 6
β’ {π β Top β£ π = βͺ
π} β π«
π« π |
| 19 | 10, 18 | ssexi 5323 |
. . . . 5
β’ {π β Top β£ π = βͺ
π} β
V |
| 20 | 7, 8, 19 | fvmpt3i 7004 |
. . . 4
β’ (π΅ β V β
(TopOnβπ΅) = {π β Top β£ π΅ = βͺ
π}) |
| 21 | 20 | eleq2d 2820 |
. . 3
β’ (π΅ β V β (π½ β (TopOnβπ΅) β π½ β {π β Top β£ π΅ = βͺ π})) |
| 22 | | unieq 4920 |
. . . . 5
β’ (π = π½ β βͺ π = βͺ
π½) |
| 23 | 22 | eqeq2d 2744 |
. . . 4
β’ (π = π½ β (π΅ = βͺ π β π΅ = βͺ π½)) |
| 24 | 23 | elrab 3684 |
. . 3
β’ (π½ β {π β Top β£ π΅ = βͺ π} β (π½ β Top β§ π΅ = βͺ π½)) |
| 25 | 21, 24 | bitrdi 287 |
. 2
β’ (π΅ β V β (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½))) |
| 26 | 1, 5, 25 | pm5.21nii 380 |
1
β’ (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½)) |
