Step | Hyp | Ref
| Expression |
1 | | qtoptopon 23071 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) |
2 | | topontop 22278 |
. . 3
β’ ((π½ qTop πΉ) β (TopOnβπ) β (π½ qTop πΉ) β Top) |
3 | | eqid 2733 |
. . . 4
β’ βͺ (π½
qTop πΉ) = βͺ (π½
qTop πΉ) |
4 | 3 | iscld 22394 |
. . 3
β’ ((π½ qTop πΉ) β Top β (π΄ β (Clsdβ(π½ qTop πΉ)) β (π΄ β βͺ (π½ qTop πΉ) β§ (βͺ (π½ qTop πΉ) β π΄) β (π½ qTop πΉ)))) |
5 | 1, 2, 4 | 3syl 18 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β (Clsdβ(π½ qTop πΉ)) β (π΄ β βͺ (π½ qTop πΉ) β§ (βͺ (π½ qTop πΉ) β π΄) β (π½ qTop πΉ)))) |
6 | | toponuni 22279 |
. . . . 5
β’ ((π½ qTop πΉ) β (TopOnβπ) β π = βͺ (π½ qTop πΉ)) |
7 | 1, 6 | syl 17 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β π = βͺ (π½ qTop πΉ)) |
8 | 7 | sseq2d 3977 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β π β π΄ β βͺ (π½ qTop πΉ))) |
9 | 7 | difeq1d 4082 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π β π΄) = (βͺ (π½ qTop πΉ) β π΄)) |
10 | 9 | eleq1d 2819 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ((π β π΄) β (π½ qTop πΉ) β (βͺ
(π½ qTop πΉ) β π΄) β (π½ qTop πΉ))) |
11 | 8, 10 | anbi12d 632 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ((π΄ β π β§ (π β π΄) β (π½ qTop πΉ)) β (π΄ β βͺ (π½ qTop πΉ) β§ (βͺ (π½ qTop πΉ) β π΄) β (π½ qTop πΉ)))) |
12 | | elqtop3 23070 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ((π β π΄) β (π½ qTop πΉ) β ((π β π΄) β π β§ (β‘πΉ β (π β π΄)) β π½))) |
13 | 12 | adantr 482 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β ((π β π΄) β (π½ qTop πΉ) β ((π β π΄) β π β§ (β‘πΉ β (π β π΄)) β π½))) |
14 | | difss 4092 |
. . . . . 6
β’ (π β π΄) β π |
15 | 14 | biantrur 532 |
. . . . 5
β’ ((β‘πΉ β (π β π΄)) β π½ β ((π β π΄) β π β§ (β‘πΉ β (π β π΄)) β π½)) |
16 | | fofun 6758 |
. . . . . . . . . 10
β’ (πΉ:πβontoβπ β Fun πΉ) |
17 | 16 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β Fun πΉ) |
18 | | funcnvcnv 6569 |
. . . . . . . . 9
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
19 | | imadif 6586 |
. . . . . . . . 9
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (π β π΄)) = ((β‘πΉ β π) β (β‘πΉ β π΄))) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β (β‘πΉ β (π β π΄)) = ((β‘πΉ β π) β (β‘πΉ β π΄))) |
21 | | fof 6757 |
. . . . . . . . . . . 12
β’ (πΉ:πβontoβπ β πΉ:πβΆπ) |
22 | | fimacnv 6691 |
. . . . . . . . . . . 12
β’ (πΉ:πβΆπ β (β‘πΉ β π) = π) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
β’ (πΉ:πβontoβπ β (β‘πΉ β π) = π) |
24 | 23 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β (β‘πΉ β π) = π) |
25 | | toponuni 22279 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β π = βͺ π½) |
27 | 24, 26 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β (β‘πΉ β π) = βͺ π½) |
28 | 27 | difeq1d 4082 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β ((β‘πΉ β π) β (β‘πΉ β π΄)) = (βͺ π½ β (β‘πΉ β π΄))) |
29 | 20, 28 | eqtrd 2773 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β (β‘πΉ β (π β π΄)) = (βͺ π½ β (β‘πΉ β π΄))) |
30 | 29 | eleq1d 2819 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β ((β‘πΉ β (π β π΄)) β π½ β (βͺ π½ β (β‘πΉ β π΄)) β π½)) |
31 | | topontop 22278 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π½ β Top) |
32 | 31 | ad2antrr 725 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β π½ β Top) |
33 | | cnvimass 6034 |
. . . . . . . . 9
β’ (β‘πΉ β π΄) β dom πΉ |
34 | | fofn 6759 |
. . . . . . . . . . 11
β’ (πΉ:πβontoβπ β πΉ Fn π) |
35 | 34 | fndmd 6608 |
. . . . . . . . . 10
β’ (πΉ:πβontoβπ β dom πΉ = π) |
36 | 35 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β dom πΉ = π) |
37 | 33, 36 | sseqtrid 3997 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β (β‘πΉ β π΄) β π) |
38 | 37, 26 | sseqtrd 3985 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β (β‘πΉ β π΄) β βͺ π½) |
39 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
40 | 39 | iscld2 22395 |
. . . . . . 7
β’ ((π½ β Top β§ (β‘πΉ β π΄) β βͺ π½) β ((β‘πΉ β π΄) β (Clsdβπ½) β (βͺ π½ β (β‘πΉ β π΄)) β π½)) |
41 | 32, 38, 40 | syl2anc 585 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β ((β‘πΉ β π΄) β (Clsdβπ½) β (βͺ π½ β (β‘πΉ β π΄)) β π½)) |
42 | 30, 41 | bitr4d 282 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β ((β‘πΉ β (π β π΄)) β π½ β (β‘πΉ β π΄) β (Clsdβπ½))) |
43 | 15, 42 | bitr3id 285 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β (((π β π΄) β π β§ (β‘πΉ β (π β π΄)) β π½) β (β‘πΉ β π΄) β (Clsdβπ½))) |
44 | 13, 43 | bitrd 279 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β§ π΄ β π) β ((π β π΄) β (π½ qTop πΉ) β (β‘πΉ β π΄) β (Clsdβπ½))) |
45 | 44 | pm5.32da 580 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ((π΄ β π β§ (π β π΄) β (π½ qTop πΉ)) β (π΄ β π β§ (β‘πΉ β π΄) β (Clsdβπ½)))) |
46 | 5, 11, 45 | 3bitr2d 307 |
1
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β (Clsdβ(π½ qTop πΉ)) β (π΄ β π β§ (β‘πΉ β π΄) β (Clsdβπ½)))) |