Step | Hyp | Ref
| Expression |
1 | | cnconst2 22786 |
. . . 4
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
2 | 1 | 3expa 1118 |
. . 3
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
3 | 2 | fmpttd 7114 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π₯ β π β¦ (π Γ {π₯})):πβΆ(π
Cn π)) |
4 | | eqid 2732 |
. . . . . 6
β’ βͺ π
=
βͺ π
|
5 | | eqid 2732 |
. . . . . 6
β’ {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp} = {π§ β
π« βͺ π
β£ (π
βΎt π§) β Comp} |
6 | | eqid 2732 |
. . . . . 6
β’ (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) |
7 | 4, 5, 6 | xkobval 23089 |
. . . . 5
β’ ran
(π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = {π¦ β£ βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£})} |
8 | 7 | eqabri 2877 |
. . . 4
β’ (π¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£})) |
9 | 2 | ad5ant15 757 |
. . . . . . . . . . . 12
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
10 | | simplr 767 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β π = β
) |
11 | 10 | imaeq2d 6059 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β ((π Γ {π₯}) β π) = ((π Γ {π₯}) β β
)) |
12 | | ima0 6076 |
. . . . . . . . . . . . . 14
β’ ((π Γ {π₯}) β β
) =
β
|
13 | | 0ss 4396 |
. . . . . . . . . . . . . 14
β’ β
β π£ |
14 | 12, 13 | eqsstri 4016 |
. . . . . . . . . . . . 13
β’ ((π Γ {π₯}) β β
) β π£ |
15 | 11, 14 | eqsstrdi 4036 |
. . . . . . . . . . . 12
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β ((π Γ {π₯}) β π) β π£) |
16 | | imaeq1 6054 |
. . . . . . . . . . . . . 14
β’ (π = (π Γ {π₯}) β (π β π) = ((π Γ {π₯}) β π)) |
17 | 16 | sseq1d 4013 |
. . . . . . . . . . . . 13
β’ (π = (π Γ {π₯}) β ((π β π) β π£ β ((π Γ {π₯}) β π) β π£)) |
18 | 17 | elrab 3683 |
. . . . . . . . . . . 12
β’ ((π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£} β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£)) |
19 | 9, 15, 18 | sylanbrc 583 |
. . . . . . . . . . 11
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β§ π₯ β π) β (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}) |
20 | 19 | ralrimiva 3146 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β βπ₯ β π (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}) |
21 | | rabid2 3464 |
. . . . . . . . . 10
β’ (π = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β βπ₯ β π (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}) |
22 | 20, 21 | sylibr 233 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β π = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}}) |
23 | | simpllr 774 |
. . . . . . . . . . 11
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β (TopOnβπ)) |
24 | | toponmax 22427 |
. . . . . . . . . . 11
β’ (π β (TopOnβπ) β π β π) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β π) |
26 | 25 | adantr 481 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β π β π) |
27 | 22, 26 | eqeltrrd 2834 |
. . . . . . . 8
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π = β
) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π) |
28 | | ifnefalse 4540 |
. . . . . . . . . . . . . . 15
β’ (π β β
β if(π = β
, π, π£) = π£) |
29 | 28 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β if(π = β
, π, π£) = π£) |
30 | 29 | eleq2d 2819 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β if(π = β
, π, π£) β π₯ β π£)) |
31 | | vex 3478 |
. . . . . . . . . . . . . . . 16
β’ π₯ β V |
32 | 31 | snss 4789 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π£ β {π₯} β π£) |
33 | 30, 32 | bitrdi 286 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β if(π = β
, π, π£) β {π₯} β π£)) |
34 | | df-ima 5689 |
. . . . . . . . . . . . . . . . 17
β’ ((π Γ {π₯}) β π) = ran ((π Γ {π₯}) βΎ π) |
35 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π β π« βͺ π
) |
36 | 35 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π β π« βͺ π
) |
37 | 36 | elpwid 4611 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π β βͺ π
) |
38 | | toponuni 22415 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π
β (TopOnβπ) β π = βͺ π
) |
39 | 38 | ad5antr 732 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π = βͺ π
) |
40 | 37, 39 | sseqtrrd 4023 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β π β π) |
41 | | xpssres 6018 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β ((π Γ {π₯}) βΎ π) = (π Γ {π₯})) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ((π Γ {π₯}) βΎ π) = (π Γ {π₯})) |
43 | 42 | rneqd 5937 |
. . . . . . . . . . . . . . . . 17
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ran ((π Γ {π₯}) βΎ π) = ran (π Γ {π₯})) |
44 | 34, 43 | eqtrid 2784 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ((π Γ {π₯}) β π) = ran (π Γ {π₯})) |
45 | | rnxp 6169 |
. . . . . . . . . . . . . . . . 17
β’ (π β β
β ran (π Γ {π₯}) = {π₯}) |
46 | 45 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ran (π Γ {π₯}) = {π₯}) |
47 | 44, 46 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β ((π Γ {π₯}) β π) = {π₯}) |
48 | 47 | sseq1d 4013 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (((π Γ {π₯}) β π) β π£ β {π₯} β π£)) |
49 | 2 | ad5ant15 757 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π Γ {π₯}) β (π
Cn π)) |
50 | 49 | biantrurd 533 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (((π Γ {π₯}) β π) β π£ β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£))) |
51 | 33, 48, 50 | 3bitr2d 306 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β if(π = β
, π, π£) β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£))) |
52 | 30, 51 | bitr3d 280 |
. . . . . . . . . . . 12
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β π£ β ((π Γ {π₯}) β (π
Cn π) β§ ((π Γ {π₯}) β π) β π£))) |
53 | 52, 18 | bitr4di 288 |
. . . . . . . . . . 11
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β§ π₯ β π) β (π₯ β π£ β (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£})) |
54 | 53 | rabbi2dva 4217 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β (π β© π£) = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}}) |
55 | | simplrr 776 |
. . . . . . . . . . . . 13
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π£ β π) |
56 | | toponss 22428 |
. . . . . . . . . . . . 13
β’ ((π β (TopOnβπ) β§ π£ β π) β π£ β π) |
57 | 23, 55, 56 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β π£ β π) |
58 | 57 | adantr 481 |
. . . . . . . . . . 11
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β π£ β π) |
59 | | sseqin2 4215 |
. . . . . . . . . . 11
β’ (π£ β π β (π β© π£) = π£) |
60 | 58, 59 | sylib 217 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β (π β© π£) = π£) |
61 | 54, 60 | eqtr3d 2774 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} = π£) |
62 | 55 | adantr 481 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β π£ β π) |
63 | 61, 62 | eqeltrd 2833 |
. . . . . . . 8
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β§ π β β
) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π) |
64 | 27, 63 | pm2.61dane 3029 |
. . . . . . 7
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π) |
65 | | imaeq2 6055 |
. . . . . . . . 9
β’ (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) = (β‘(π₯ β π β¦ (π Γ {π₯})) β {π β (π
Cn π) β£ (π β π) β π£})) |
66 | | eqid 2732 |
. . . . . . . . . 10
β’ (π₯ β π β¦ (π Γ {π₯})) = (π₯ β π β¦ (π Γ {π₯})) |
67 | 66 | mptpreima 6237 |
. . . . . . . . 9
β’ (β‘(π₯ β π β¦ (π Γ {π₯})) β {π β (π
Cn π) β£ (π β π) β π£}) = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} |
68 | 65, 67 | eqtrdi 2788 |
. . . . . . . 8
β’ (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) = {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}}) |
69 | 68 | eleq1d 2818 |
. . . . . . 7
β’ (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β ((β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π β {π₯ β π β£ (π Γ {π₯}) β {π β (π
Cn π) β£ (π β π) β π£}} β π)) |
70 | 64, 69 | syl5ibrcom 246 |
. . . . . 6
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β§ (π
βΎt π) β Comp) β (π¦ = {π β (π
Cn π) β£ (π β π) β π£} β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
71 | 70 | expimpd 454 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β π)) β (((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£}) β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
72 | 71 | rexlimdvva 3211 |
. . . 4
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (βπ β π« βͺ π
βπ£ β π ((π
βΎt π) β Comp β§ π¦ = {π β (π
Cn π) β£ (π β π) β π£}) β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
73 | 8, 72 | biimtrid 241 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β (β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π)) |
74 | 73 | ralrimiv 3145 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β βπ¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})(β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π) |
75 | | simpr 485 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β π β (TopOnβπ)) |
76 | | ovex 7441 |
. . . . . 6
β’ (π
Cn π) β V |
77 | 76 | pwex 5378 |
. . . . 5
β’ π«
(π
Cn π) β V |
78 | 4, 5, 6 | xkotf 23088 |
. . . . . 6
β’ (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}):({π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp} Γ π)βΆπ« (π
Cn π) |
79 | | frn 6724 |
. . . . . 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 5322 |
. . . 4
β’ ran
(π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β V |
82 | 81 | a1i 11 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β V) |
83 | | topontop 22414 |
. . . 4
β’ (π
β (TopOnβπ) β π
β Top) |
84 | | topontop 22414 |
. . . 4
β’ (π β (TopOnβπ) β π β Top) |
85 | 4, 5, 6 | xkoval 23090 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π βko π
) = (topGenβ(fiβran
(π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})))) |
86 | 83, 84, 85 | syl2an 596 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π βko π
) = (topGenβ(fiβran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})))) |
87 | | eqid 2732 |
. . . . 5
β’ (π βko π
) = (π βko π
) |
88 | 87 | xkotopon 23103 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π βko π
) β (TopOnβ(π
Cn π))) |
89 | 83, 84, 88 | syl2an 596 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π βko π
) β (TopOnβ(π
Cn π))) |
90 | 75, 82, 86, 89 | subbascn 22757 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((π₯ β π β¦ (π Γ {π₯})) β (π Cn (π βko π
)) β ((π₯ β π β¦ (π Γ {π₯})):πβΆ(π
Cn π) β§ βπ¦ β ran (π β {π§ β π« βͺ π
β£ (π
βΎt π§)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})(β‘(π₯ β π β¦ (π Γ {π₯})) β π¦) β π))) |
91 | 3, 74, 90 | mpbir2and 711 |
1
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π₯ β π β¦ (π Γ {π₯})) β (π Cn (π βko π
))) |