Step | Hyp | Ref
| Expression |
1 | | funtopon 13482 |
. . . . 5
β’ Fun
TopOn |
2 | | funrel 5233 |
. . . . 5
β’ (Fun
TopOn β Rel TopOn) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ Rel
TopOn |
4 | | relelfvdm 5547 |
. . . 4
β’ ((Rel
TopOn β§ π½ β
(TopOnβπ΅)) β
π΅ β dom
TopOn) |
5 | 3, 4 | mpan 424 |
. . 3
β’ (π½ β (TopOnβπ΅) β π΅ β dom TopOn) |
6 | 5 | elexd 2750 |
. 2
β’ (π½ β (TopOnβπ΅) β π΅ β V) |
7 | | uniexg 4439 |
. . . 4
β’ (π½ β Top β βͺ π½
β V) |
8 | | eleq1 2240 |
. . . 4
β’ (π΅ = βͺ
π½ β (π΅ β V β βͺ π½
β V)) |
9 | 7, 8 | syl5ibrcom 157 |
. . 3
β’ (π½ β Top β (π΅ = βͺ
π½ β π΅ β V)) |
10 | 9 | imp 124 |
. 2
β’ ((π½ β Top β§ π΅ = βͺ
π½) β π΅ β V) |
11 | | eqeq1 2184 |
. . . . . 6
β’ (π = π΅ β (π = βͺ π β π΅ = βͺ π)) |
12 | 11 | rabbidv 2726 |
. . . . 5
β’ (π = π΅ β {π β Top β£ π = βͺ π} = {π β Top β£ π΅ = βͺ π}) |
13 | | df-topon 13481 |
. . . . 5
β’ TopOn =
(π β V β¦ {π β Top β£ π = βͺ
π}) |
14 | | vpwex 4179 |
. . . . . . 7
β’ π«
π β V |
15 | 14 | pwex 4183 |
. . . . . 6
β’ π«
π« π β
V |
16 | | rabss 3232 |
. . . . . . 7
β’ ({π β Top β£ π = βͺ
π} β π«
π« π β
βπ β Top (π = βͺ
π β π β π« π« π)) |
17 | | pwuni 4192 |
. . . . . . . . . 10
β’ π β π« βͺ π |
18 | | pweq 3578 |
. . . . . . . . . 10
β’ (π = βͺ
π β π« π = π« βͺ π) |
19 | 17, 18 | sseqtrrid 3206 |
. . . . . . . . 9
β’ (π = βͺ
π β π β π« π) |
20 | | velpw 3582 |
. . . . . . . . 9
β’ (π β π« π«
π β π β π« π) |
21 | 19, 20 | sylibr 134 |
. . . . . . . 8
β’ (π = βͺ
π β π β π« π« π) |
22 | 21 | a1i 9 |
. . . . . . 7
β’ (π β Top β (π = βͺ
π β π β π« π« π)) |
23 | 16, 22 | mprgbir 2535 |
. . . . . 6
β’ {π β Top β£ π = βͺ
π} β π«
π« π |
24 | 15, 23 | ssexi 4141 |
. . . . 5
β’ {π β Top β£ π = βͺ
π} β
V |
25 | 12, 13, 24 | fvmpt3i 5596 |
. . . 4
β’ (π΅ β V β
(TopOnβπ΅) = {π β Top β£ π΅ = βͺ
π}) |
26 | 25 | eleq2d 2247 |
. . 3
β’ (π΅ β V β (π½ β (TopOnβπ΅) β π½ β {π β Top β£ π΅ = βͺ π})) |
27 | | unieq 3818 |
. . . . 5
β’ (π = π½ β βͺ π = βͺ
π½) |
28 | 27 | eqeq2d 2189 |
. . . 4
β’ (π = π½ β (π΅ = βͺ π β π΅ = βͺ π½)) |
29 | 28 | elrab 2893 |
. . 3
β’ (π½ β {π β Top β£ π΅ = βͺ π} β (π½ β Top β§ π΅ = βͺ π½)) |
30 | 26, 29 | bitrdi 196 |
. 2
β’ (π΅ β V β (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½))) |
31 | 6, 10, 30 | pm5.21nii 704 |
1
β’ (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½)) |