Step | Hyp | Ref
| Expression |
1 | | cnconst2 22657 |
. . . 4
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
2 | 1 | 3expa 1119 |
. . 3
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
3 | 2 | fmpttd 7067 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π₯ β π β¦ (π Γ {π₯})):πβΆ(π
Cn π)) |
4 | | eqid 2733 |
. . . . . 6
β’ βͺ π
=
βͺ π
|
5 | | eqid 2733 |
. . . . . 6
β’ {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp} = {π§ β
π« βͺ π
β£ (π
βΎt π§) β Comp} |
6 | | eqid 2733 |
. . . . . 6
β’ (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) |
7 | 4, 5, 6 | xkobval 22960 |
. . . . 5
β’ ran
(π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = {π¦ β£ βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£})} |
8 | 7 | eqabi 2878 |
. . . 4
β’ (π¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£})) |
9 | 2 | ad5ant15 758 |
. . . . . . . . . . . 12
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
10 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β π = β
) |
11 | 10 | imaeq2d 6017 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β ((π Γ {π₯}) β π) = ((π Γ {π₯}) β β
)) |
12 | | ima0 6033 |
. . . . . . . . . . . . . 14
β’ ((π Γ {π₯}) β β
) =
β
|
13 | | 0ss 4360 |
. . . . . . . . . . . . . 14
β’ β
β π£ |
14 | 12, 13 | eqsstri 3982 |
. . . . . . . . . . . . 13
β’ ((π Γ {π₯}) β β
) β π£ |
15 | 11, 14 | eqsstrdi 4002 |
. . . . . . . . . . . 12
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β ((π Γ {π₯}) β π) β π£) |
16 | | imaeq1 6012 |
. . . . . . . . . . . . . 14
β’ (π = (π Γ {π₯}) β (π β π) = ((π Γ {π₯}) β π)) |
17 | 16 | sseq1d 3979 |
. . . . . . . . . . . . 13
β’ (π = (π Γ {π₯}) β ((π β π) β π£ β ((π Γ {π₯}) β π) β π£)) |
18 | 17 | elrab 3649 |
. . . . . . . . . . . 12
β’ ((π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£} β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£)) |
19 | 9, 15, 18 | sylanbrc 584 |
. . . . . . . . . . 11
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}) |
20 | 19 | ralrimiva 3140 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β βπ₯ β π (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}) |
21 | | rabid2 3438 |
. . . . . . . . . 10
β’ (π = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β βπ₯ β π (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}) |
22 | 20, 21 | sylibr 233 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β π = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}}) |
23 | | simpllr 775 |
. . . . . . . . . . 11
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β (TopOnβπ)) |
24 | | toponmax 22298 |
. . . . . . . . . . 11
β’ (π β (TopOnβπ) β π β π) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β π) |
26 | 25 | adantr 482 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β π β π) |
27 | 22, 26 | eqeltrrd 2835 |
. . . . . . . 8
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π) |
28 | | ifnefalse 4502 |
. . . . . . . . . . . . . . 15
β’ (π β β
β if(π = β
, π, π£) = π£) |
29 | 28 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β if(π = β
, π, π£) = π£) |
30 | 29 | eleq2d 2820 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β if(π = β
, π, π£) β π₯ β π£)) |
31 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π₯ β V |
32 | 31 | snss 4750 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π£ β {π₯} β π£) |
33 | 30, 32 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β if(π = β
, π, π£) β {π₯} β π£)) |
34 | | df-ima 5650 |
. . . . . . . . . . . . . . . . 17
β’ ((π Γ {π₯}) β π) = ran ((π Γ {π₯}) βΎ π) |
35 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β π« βͺ π
) |
36 | 35 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π β π« βͺ π
) |
37 | 36 | elpwid 4573 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π β βͺ π
) |
38 | | toponuni 22286 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π
β (TopOnβπ) β π = βͺ π
) |
39 | 38 | ad5antr 733 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π = βͺ π
) |
40 | 37, 39 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π β π) |
41 | | xpssres 5978 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β ((π Γ {π₯}) βΎ π) = (π Γ {π₯})) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ((π Γ {π₯}) βΎ π) = (π Γ {π₯})) |
43 | 42 | rneqd 5897 |
. . . . . . . . . . . . . . . . 17
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ran ((π Γ {π₯}) βΎ π) = ran (π Γ {π₯})) |
44 | 34, 43 | eqtrid 2785 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ((π Γ {π₯}) β π) = ran (π Γ {π₯})) |
45 | | rnxp 6126 |
. . . . . . . . . . . . . . . . 17
β’ (π β β
β ran (π Γ {π₯}) = {π₯}) |
46 | 45 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ran (π Γ {π₯}) = {π₯}) |
47 | 44, 46 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ((π Γ {π₯}) β π) = {π₯}) |
48 | 47 | sseq1d 3979 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (((π Γ {π₯}) β π) β π£ β {π₯} β π£)) |
49 | 2 | ad5ant15 758 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
50 | 49 | biantrurd 534 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (((π Γ {π₯}) β π) β π£ β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£))) |
51 | 33, 48, 50 | 3bitr2d 307 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β if(π = β
, π, π£) β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£))) |
52 | 30, 51 | bitr3d 281 |
. . . . . . . . . . . 12
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β π£ β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£))) |
53 | 52, 18 | bitr4di 289 |
. . . . . . . . . . 11
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β π£ β (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£})) |
54 | 53 | rabbi2dva 4181 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β (π β© π£) = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}}) |
55 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π£ β π) |
56 | | toponss 22299 |
. . . . . . . . . . . . 13
β’ ((π β (TopOnβπ) β§ π£ β π) β π£ β π) |
57 | 23, 55, 56 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π£ β π) |
58 | 57 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β π£ β π) |
59 | | sseqin2 4179 |
. . . . . . . . . . 11
β’ (π£ β π β (π β© π£) = π£) |
60 | 58, 59 | sylib 217 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β (π β© π£) = π£) |
61 | 54, 60 | eqtr3d 2775 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} = π£) |
62 | 55 | adantr 482 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β π£ β π) |
63 | 61, 62 | eqeltrd 2834 |
. . . . . . . 8
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π) |
64 | 27, 63 | pm2.61dane 3029 |
. . . . . . 7
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π) |
65 | | imaeq2 6013 |
. . . . . . . . 9
β’ (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) = (β‘(π₯ β π β¦ (π Γ {π₯})) β {π β (π
Cn π) β£ (π β π) β π£})) |
66 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π β¦ (π Γ {π₯})) = (π₯ β π β¦ (π Γ {π₯})) |
67 | 66 | mptpreima 6194 |
. . . . . . . . 9
β’ (β‘(π₯ β π β¦ (π Γ {π₯})) β {π β (π
Cn π) β£ (π β π) β π£}) = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} |
68 | 65, 67 | eqtrdi 2789 |
. . . . . . . 8
β’ (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}}) |
69 | 68 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β ((β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π)) |
70 | 64, 69 | syl5ibrcom 247 |
. . . . . 6
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
71 | 70 | expimpd 455 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β (((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£}) β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
72 | 71 | rexlimdvva 3202 |
. . . 4
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£}) β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
73 | 8, 72 | biimtrid 241 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
74 | 73 | ralrimiv 3139 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β βπ¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})(β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π) |
75 | | simpr 486 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β π β (TopOnβπ)) |
76 | | ovex 7394 |
. . . . . 6
β’ (π
Cn π) β V |
77 | 76 | pwex 5339 |
. . . . 5
β’ π«
(π
Cn π) β V |
78 | 4, 5, 6 | xkotf 22959 |
. . . . . 6
β’ (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}):({π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp} Γ π)βΆπ« (π
Cn π) |
79 | | frn 6679 |
. . . . . 6
β’ ((π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}):({π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp} Γ π)βΆπ« (π
Cn π) β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β π« (π
Cn π)) |
80 | 78, 79 | ax-mp 5 |
. . . . 5
β’ ran
(π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β π« (π
Cn π) |
81 | 77, 80 | ssexi 5283 |
. . . 4
β’ ran
(π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β V |
82 | 81 | a1i 11 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β V) |
83 | | topontop 22285 |
. . . 4
β’ (π
β (TopOnβπ) β π
β Top) |
84 | | topontop 22285 |
. . . 4
β’ (π β (TopOnβπ) β π β Top) |
85 | 4, 5, 6 | xkoval 22961 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π βko π
) = (topGenβ(fiβran
(π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})))) |
86 | 83, 84, 85 | syl2an 597 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π βko π
) = (topGenβ(fiβran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})))) |
87 | | eqid 2733 |
. . . . 5
β’ (π βko π
) = (π βko π
) |
88 | 87 | xkotopon 22974 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π βko π
) β (TopOnβ(π
Cn π))) |
89 | 83, 84, 88 | syl2an 597 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π βko π
) β (TopOnβ(π
Cn π))) |
90 | 75, 82, 86, 89 | subbascn 22628 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((π₯ β π β¦ (π Γ {π₯})) β (π Cn (π βko π
)) β ((π₯ β π β¦ (π Γ {π₯})):πβΆ(π
Cn π) β§ βπ¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})(β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π))) |
91 | 3, 74, 90 | mpbir2and 712 |
1
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π₯ β π β¦ (π Γ {π₯})) β (π Cn (π βko π
))) |