Step | Hyp | Ref
| Expression |
1 | | elfvex 6885 |
. 2
β’ (π½ β (TopOnβπ΅) β π΅ β V) |
2 | | uniexg 7682 |
. . . 4
β’ (π½ β Top β βͺ π½
β V) |
3 | | eleq1 2826 |
. . . 4
β’ (π΅ = βͺ
π½ β (π΅ β V β βͺ π½
β V)) |
4 | 2, 3 | syl5ibrcom 247 |
. . 3
β’ (π½ β Top β (π΅ = βͺ
π½ β π΅ β V)) |
5 | 4 | imp 408 |
. 2
β’ ((π½ β Top β§ π΅ = βͺ
π½) β π΅ β V) |
6 | | eqeq1 2741 |
. . . . . 6
β’ (π = π΅ β (π = βͺ π β π΅ = βͺ π)) |
7 | 6 | rabbidv 3418 |
. . . . 5
β’ (π = π΅ β {π β Top β£ π = βͺ π} = {π β Top β£ π΅ = βͺ π}) |
8 | | df-topon 22276 |
. . . . 5
β’ TopOn =
(π β V β¦ {π β Top β£ π = βͺ
π}) |
9 | | vpwex 5337 |
. . . . . . 7
β’ π«
π β V |
10 | 9 | pwex 5340 |
. . . . . 6
β’ π«
π« π β
V |
11 | | rabss 4034 |
. . . . . . 7
β’ ({π β Top β£ π = βͺ
π} β π«
π« π β
βπ β Top (π = βͺ
π β π β π« π« π)) |
12 | | pwuni 4911 |
. . . . . . . . . 10
β’ π β π« βͺ π |
13 | | pweq 4579 |
. . . . . . . . . 10
β’ (π = βͺ
π β π« π = π« βͺ π) |
14 | 12, 13 | sseqtrrid 4002 |
. . . . . . . . 9
β’ (π = βͺ
π β π β π« π) |
15 | | velpw 4570 |
. . . . . . . . 9
β’ (π β π« π«
π β π β π« π) |
16 | 14, 15 | sylibr 233 |
. . . . . . . 8
β’ (π = βͺ
π β π β π« π« π) |
17 | 16 | a1i 11 |
. . . . . . 7
β’ (π β Top β (π = βͺ
π β π β π« π« π)) |
18 | 11, 17 | mprgbir 3072 |
. . . . . 6
β’ {π β Top β£ π = βͺ
π} β π«
π« π |
19 | 10, 18 | ssexi 5284 |
. . . . 5
β’ {π β Top β£ π = βͺ
π} β
V |
20 | 7, 8, 19 | fvmpt3i 6958 |
. . . 4
β’ (π΅ β V β
(TopOnβπ΅) = {π β Top β£ π΅ = βͺ
π}) |
21 | 20 | eleq2d 2824 |
. . 3
β’ (π΅ β V β (π½ β (TopOnβπ΅) β π½ β {π β Top β£ π΅ = βͺ π})) |
22 | | unieq 4881 |
. . . . 5
β’ (π = π½ β βͺ π = βͺ
π½) |
23 | 22 | eqeq2d 2748 |
. . . 4
β’ (π = π½ β (π΅ = βͺ π β π΅ = βͺ π½)) |
24 | 23 | elrab 3650 |
. . 3
β’ (π½ β {π β Top β£ π΅ = βͺ π} β (π½ β Top β§ π΅ = βͺ π½)) |
25 | 21, 24 | bitrdi 287 |
. 2
β’ (π΅ β V β (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½))) |
26 | 1, 5, 25 | pm5.21nii 380 |
1
β’ (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½)) |