Step | Hyp | Ref
| Expression |
1 | | xkoco1cn.f |
. . . 4
β’ (π β πΉ β (π
Cn π)) |
2 | | cnco 22640 |
. . . 4
β’ ((πΉ β (π
Cn π) β§ π β (π Cn π)) β (π β πΉ) β (π
Cn π)) |
3 | 1, 2 | sylan 581 |
. . 3
β’ ((π β§ π β (π Cn π)) β (π β πΉ) β (π
Cn π)) |
4 | 3 | fmpttd 7067 |
. 2
β’ (π β (π β (π Cn π) β¦ (π β πΉ)):(π Cn π)βΆ(π
Cn π)) |
5 | | eqid 2733 |
. . . . . 6
β’ βͺ π
=
βͺ π
|
6 | | eqid 2733 |
. . . . . 6
β’ {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp} = {π¦ β
π« βͺ π
β£ (π
βΎt π¦) β Comp} |
7 | | eqid 2733 |
. . . . . 6
β’ (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) = (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) |
8 | 5, 6, 7 | xkobval 22960 |
. . . . 5
β’ ran
(π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) = {π₯ β£ βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π₯ = {β β (π
Cn π) β£ (β β π) β π£})} |
9 | 8 | eqabi 2878 |
. . . 4
β’ (π₯ β ran (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) β βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π₯ = {β β (π
Cn π) β£ (β β π) β π£})) |
10 | 1 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β πΉ β (π
Cn π)) |
11 | 10, 2 | sylan 581 |
. . . . . . . . . 10
β’ ((((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β (π Cn π)) β (π β πΉ) β (π
Cn π)) |
12 | | imaeq1 6012 |
. . . . . . . . . . . . 13
β’ (β = (π β πΉ) β (β β π) = ((π β πΉ) β π)) |
13 | | imaco 6207 |
. . . . . . . . . . . . 13
β’ ((π β πΉ) β π) = (π β (πΉ β π)) |
14 | 12, 13 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (β = (π β πΉ) β (β β π) = (π β (πΉ β π))) |
15 | 14 | sseq1d 3979 |
. . . . . . . . . . 11
β’ (β = (π β πΉ) β ((β β π) β π£ β (π β (πΉ β π)) β π£)) |
16 | 15 | elrab3 3650 |
. . . . . . . . . 10
β’ ((π β πΉ) β (π
Cn π) β ((π β πΉ) β {β β (π
Cn π) β£ (β β π) β π£} β (π β (πΉ β π)) β π£)) |
17 | 11, 16 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β (π Cn π)) β ((π β πΉ) β {β β (π
Cn π) β£ (β β π) β π£} β (π β (πΉ β π)) β π£)) |
18 | 17 | rabbidva 3413 |
. . . . . . . 8
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β {π β (π Cn π) β£ (π β πΉ) β {β β (π
Cn π) β£ (β β π) β π£}} = {π β (π Cn π) β£ (π β (πΉ β π)) β π£}) |
19 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π =
βͺ π |
20 | | cntop2 22615 |
. . . . . . . . . . 11
β’ (πΉ β (π
Cn π) β π β Top) |
21 | 1, 20 | syl 17 |
. . . . . . . . . 10
β’ (π β π β Top) |
22 | 21 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β Top) |
23 | | xkoco1cn.t |
. . . . . . . . . 10
β’ (π β π β Top) |
24 | 23 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β Top) |
25 | | imassrn 6028 |
. . . . . . . . . 10
β’ (πΉ β π) β ran πΉ |
26 | 5, 19 | cnf 22620 |
. . . . . . . . . . 11
β’ (πΉ β (π
Cn π) β πΉ:βͺ π
βΆβͺ π) |
27 | | frn 6679 |
. . . . . . . . . . 11
β’ (πΉ:βͺ
π
βΆβͺ π
β ran πΉ β βͺ π) |
28 | 10, 26, 27 | 3syl 18 |
. . . . . . . . . 10
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β ran πΉ β βͺ π) |
29 | 25, 28 | sstrid 3959 |
. . . . . . . . 9
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β (πΉ β π) β βͺ π) |
30 | | imacmp 22771 |
. . . . . . . . . 10
β’ ((πΉ β (π
Cn π) β§ (π
βΎt π) β Comp) β (π βΎt (πΉ β π)) β Comp) |
31 | 10, 30 | sylancom 589 |
. . . . . . . . 9
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β (π βΎt (πΉ β π)) β Comp) |
32 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π£ β π) |
33 | 19, 22, 24, 29, 31, 32 | xkoopn 22963 |
. . . . . . . 8
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β {π β (π Cn π) β£ (π β (πΉ β π)) β π£} β (π βko π)) |
34 | 18, 33 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β {π β (π Cn π) β£ (π β πΉ) β {β β (π
Cn π) β£ (β β π) β π£}} β (π βko π)) |
35 | | imaeq2 6013 |
. . . . . . . . 9
β’ (π₯ = {β β (π
Cn π) β£ (β β π) β π£} β (β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) = (β‘(π β (π Cn π) β¦ (π β πΉ)) β {β β (π
Cn π) β£ (β β π) β π£})) |
36 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β (π Cn π) β¦ (π β πΉ)) = (π β (π Cn π) β¦ (π β πΉ)) |
37 | 36 | mptpreima 6194 |
. . . . . . . . 9
β’ (β‘(π β (π Cn π) β¦ (π β πΉ)) β {β β (π
Cn π) β£ (β β π) β π£}) = {π β (π Cn π) β£ (π β πΉ) β {β β (π
Cn π) β£ (β β π) β π£}} |
38 | 35, 37 | eqtrdi 2789 |
. . . . . . . 8
β’ (π₯ = {β β (π
Cn π) β£ (β β π) β π£} β (β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) = {π β (π Cn π) β£ (π β πΉ) β {β β (π
Cn π) β£ (β β π) β π£}}) |
39 | 38 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = {β β (π
Cn π) β£ (β β π) β π£} β ((β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) β (π βko π) β {π β (π Cn π) β£ (π β πΉ) β {β β (π
Cn π) β£ (β β π) β π£}} β (π βko π))) |
40 | 34, 39 | syl5ibrcom 247 |
. . . . . 6
β’ (((π β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β (π₯ = {β β (π
Cn π) β£ (β β π) β π£} β (β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) β (π βko π))) |
41 | 40 | expimpd 455 |
. . . . 5
β’ ((π β§ (π β π« βͺ π
β§ π£ β π)) β (((π
βΎt π) β Comp β§ π₯ = {β β (π
Cn π) β£ (β β π) β π£}) β (β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) β (π βko π))) |
42 | 41 | rexlimdvva 3202 |
. . . 4
β’ (π β (βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π₯ = {β β (π
Cn π) β£ (β β π) β π£}) β (β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) β (π βko π))) |
43 | 9, 42 | biimtrid 241 |
. . 3
β’ (π β (π₯ β ran (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) β (β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) β (π βko π))) |
44 | 43 | ralrimiv 3139 |
. 2
β’ (π β βπ₯ β ran (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£})(β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) β (π βko π)) |
45 | | eqid 2733 |
. . . . 5
β’ (π βko π) = (π βko π) |
46 | 45 | xkotopon 22974 |
. . . 4
β’ ((π β Top β§ π β Top) β (π βko π) β (TopOnβ(π Cn π))) |
47 | 21, 23, 46 | syl2anc 585 |
. . 3
β’ (π β (π βko π) β (TopOnβ(π Cn π))) |
48 | | ovex 7394 |
. . . . . 6
β’ (π
Cn π) β V |
49 | 48 | pwex 5339 |
. . . . 5
β’ π«
(π
Cn π) β V |
50 | 5, 6, 7 | xkotf 22959 |
. . . . . 6
β’ (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}):({π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp} Γ π)βΆπ« (π
Cn π) |
51 | | frn 6679 |
. . . . . 6
β’ ((π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}):({π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp} Γ π)βΆπ« (π
Cn π) β ran (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) β π« (π
Cn π)) |
52 | 50, 51 | ax-mp 5 |
. . . . 5
β’ ran
(π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) β π« (π
Cn π) |
53 | 49, 52 | ssexi 5283 |
. . . 4
β’ ran
(π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) β V |
54 | 53 | a1i 11 |
. . 3
β’ (π β ran (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£}) β V) |
55 | | cntop1 22614 |
. . . . 5
β’ (πΉ β (π
Cn π) β π
β Top) |
56 | 1, 55 | syl 17 |
. . . 4
β’ (π β π
β Top) |
57 | 5, 6, 7 | xkoval 22961 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π βko π
) = (topGenβ(fiβran
(π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£})))) |
58 | 56, 23, 57 | syl2anc 585 |
. . 3
β’ (π β (π βko π
) = (topGenβ(fiβran (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£})))) |
59 | | eqid 2733 |
. . . . 5
β’ (π βko π
) = (π βko π
) |
60 | 59 | xkotopon 22974 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π βko π
) β (TopOnβ(π
Cn π))) |
61 | 56, 23, 60 | syl2anc 585 |
. . 3
β’ (π β (π βko π
) β (TopOnβ(π
Cn π))) |
62 | 47, 54, 58, 61 | subbascn 22628 |
. 2
β’ (π β ((π β (π Cn π) β¦ (π β πΉ)) β ((π βko π) Cn (π βko π
)) β ((π β (π Cn π) β¦ (π β πΉ)):(π Cn π)βΆ(π
Cn π) β§ βπ₯ β ran (π β {π¦ β π« βͺ π
β£ (π
βΎt π¦)
β Comp}, π£ β
π β¦ {β β (π
Cn π) β£ (β β π) β π£})(β‘(π β (π Cn π) β¦ (π β πΉ)) β π₯) β (π βko π)))) |
63 | 4, 44, 62 | mpbir2and 712 |
1
β’ (π β (π β (π Cn π) β¦ (π β πΉ)) β ((π βko π) Cn (π βko π
))) |