Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β π β (TopOnβπ)) |
2 | 1 | cnmptid 23035 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β (π¦ β π β¦ π¦) β (π Cn π)) |
3 | | simpll 766 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β π
β (TopOnβπ)) |
4 | | simpr 486 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β π₯ β π) |
5 | 1, 3, 4 | cnmptc 23036 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β (π¦ β π β¦ π₯) β (π Cn π
)) |
6 | 1, 2, 5 | cnmpt1t 23039 |
. . 3
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π₯ β π) β (π¦ β π β¦ β¨π¦, π₯β©) β (π Cn (π Γt π
))) |
7 | | xkoinjcn.3 |
. . 3
β’ πΉ = (π₯ β π β¦ (π¦ β π β¦ β¨π¦, π₯β©)) |
8 | 6, 7 | fmptd 7066 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β πΉ:πβΆ(π Cn (π Γt π
))) |
9 | | eqid 2733 |
. . . . . 6
β’ βͺ π =
βͺ π |
10 | | eqid 2733 |
. . . . . 6
β’ {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp} = {π€ β
π« βͺ π β£ (π βΎt π€) β Comp} |
11 | | eqid 2733 |
. . . . . 6
β’ (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) = (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) |
12 | 9, 10, 11 | xkobval 22960 |
. . . . 5
β’ ran
(π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) = {π§ β£ βπ β π« βͺ πβπ£ β (π Γt π
)((π βΎt π) β Comp β§ π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£})} |
13 | 12 | eqabi 2878 |
. . . 4
β’ (π§ β ran (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β βπ β π« βͺ πβπ£ β (π Γt π
)((π βΎt π) β Comp β§ π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£})) |
14 | | simpll 766 |
. . . . . . . . . . . 12
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β (π
β (TopOnβπ) β§ π β (TopOnβπ))) |
15 | 14, 6 | sylan 581 |
. . . . . . . . . . 11
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β (π¦ β π β¦ β¨π¦, π₯β©) β (π Cn (π Γt π
))) |
16 | | imaeq1 6012 |
. . . . . . . . . . . . 13
β’ (π = (π¦ β π β¦ β¨π¦, π₯β©) β (π β π) = ((π¦ β π β¦ β¨π¦, π₯β©) β π)) |
17 | 16 | sseq1d 3979 |
. . . . . . . . . . . 12
β’ (π = (π¦ β π β¦ β¨π¦, π₯β©) β ((π β π) β π£ β ((π¦ β π β¦ β¨π¦, π₯β©) β π) β π£)) |
18 | 17 | elrab3 3650 |
. . . . . . . . . . 11
β’ ((π¦ β π β¦ β¨π¦, π₯β©) β (π Cn (π Γt π
)) β ((π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£} β ((π¦ β π β¦ β¨π¦, π₯β©) β π) β π£)) |
19 | 15, 18 | syl 17 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β ((π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£} β ((π¦ β π β¦ β¨π¦, π₯β©) β π) β π£)) |
20 | | funmpt 6543 |
. . . . . . . . . . 11
β’ Fun
(π¦ β π β¦ β¨π¦, π₯β©) |
21 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β π β π« βͺ π) |
22 | 21 | elpwid 4573 |
. . . . . . . . . . . . . 14
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β π β βͺ π) |
23 | 14 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β π β (TopOnβπ)) |
24 | | toponuni 22286 |
. . . . . . . . . . . . . . 15
β’ (π β (TopOnβπ) β π = βͺ π) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β π = βͺ π) |
26 | 22, 25 | sseqtrrd 3989 |
. . . . . . . . . . . . 13
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β π β π) |
27 | 26 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β π β π) |
28 | | dmmptg 6198 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
π β¨π¦, π₯β© β V β dom (π¦ β π β¦ β¨π¦, π₯β©) = π) |
29 | | opex 5425 |
. . . . . . . . . . . . . 14
β’
β¨π¦, π₯β© β V |
30 | 29 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π¦ β π β β¨π¦, π₯β© β V) |
31 | 28, 30 | mprg 3067 |
. . . . . . . . . . . 12
β’ dom
(π¦ β π β¦ β¨π¦, π₯β©) = π |
32 | 27, 31 | sseqtrrdi 3999 |
. . . . . . . . . . 11
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β π β dom (π¦ β π β¦ β¨π¦, π₯β©)) |
33 | | funimass4 6911 |
. . . . . . . . . . 11
β’ ((Fun
(π¦ β π β¦ β¨π¦, π₯β©) β§ π β dom (π¦ β π β¦ β¨π¦, π₯β©)) β (((π¦ β π β¦ β¨π¦, π₯β©) β π) β π£ β βπ§ β π ((π¦ β π β¦ β¨π¦, π₯β©)βπ§) β π£)) |
34 | 20, 32, 33 | sylancr 588 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β (((π¦ β π β¦ β¨π¦, π₯β©) β π) β π£ β βπ§ β π ((π¦ β π β¦ β¨π¦, π₯β©)βπ§) β π£)) |
35 | 27 | sselda 3948 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β§ π§ β π) β π§ β π) |
36 | | opeq1 4834 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π§ β β¨π¦, π₯β© = β¨π§, π₯β©) |
37 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π β¦ β¨π¦, π₯β©) = (π¦ β π β¦ β¨π¦, π₯β©) |
38 | | opex 5425 |
. . . . . . . . . . . . . . . 16
β’
β¨π§, π₯β© β V |
39 | 36, 37, 38 | fvmpt 6952 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β ((π¦ β π β¦ β¨π¦, π₯β©)βπ§) = β¨π§, π₯β©) |
40 | 35, 39 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β§ π§ β π) β ((π¦ β π β¦ β¨π¦, π₯β©)βπ§) = β¨π§, π₯β©) |
41 | 40 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β§ π§ β π) β (((π¦ β π β¦ β¨π¦, π₯β©)βπ§) β π£ β β¨π§, π₯β© β π£)) |
42 | | vex 3451 |
. . . . . . . . . . . . . 14
β’ π₯ β V |
43 | | opeq2 4835 |
. . . . . . . . . . . . . . 15
β’ (π€ = π₯ β β¨π§, π€β© = β¨π§, π₯β©) |
44 | 43 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π€ = π₯ β (β¨π§, π€β© β π£ β β¨π§, π₯β© β π£)) |
45 | 42, 44 | ralsn 4646 |
. . . . . . . . . . . . 13
β’
(βπ€ β
{π₯}β¨π§, π€β© β π£ β β¨π§, π₯β© β π£) |
46 | 41, 45 | bitr4di 289 |
. . . . . . . . . . . 12
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β§ π§ β π) β (((π¦ β π β¦ β¨π¦, π₯β©)βπ§) β π£ β βπ€ β {π₯}β¨π§, π€β© β π£)) |
47 | 46 | ralbidva 3169 |
. . . . . . . . . . 11
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β (βπ§ β π ((π¦ β π β¦ β¨π¦, π₯β©)βπ§) β π£ β βπ§ β π βπ€ β {π₯}β¨π§, π€β© β π£)) |
48 | | dfss3 3936 |
. . . . . . . . . . . 12
β’ ((π Γ {π₯}) β π£ β βπ‘ β (π Γ {π₯})π‘ β π£) |
49 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π‘ = β¨π§, π€β© β (π‘ β π£ β β¨π§, π€β© β π£)) |
50 | 49 | ralxp 5801 |
. . . . . . . . . . . 12
β’
(βπ‘ β
(π Γ {π₯})π‘ β π£ β βπ§ β π βπ€ β {π₯}β¨π§, π€β© β π£) |
51 | 48, 50 | bitri 275 |
. . . . . . . . . . 11
β’ ((π Γ {π₯}) β π£ β βπ§ β π βπ€ β {π₯}β¨π§, π€β© β π£) |
52 | 47, 51 | bitr4di 289 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β (βπ§ β π ((π¦ β π β¦ β¨π¦, π₯β©)βπ§) β π£ β (π Γ {π₯}) β π£)) |
53 | 19, 34, 52 | 3bitrd 305 |
. . . . . . . . 9
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π₯ β π) β ((π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£} β (π Γ {π₯}) β π£)) |
54 | 53 | rabbidva 3413 |
. . . . . . . 8
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β {π₯ β π β£ (π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£}} = {π₯ β π β£ (π Γ {π₯}) β π£}) |
55 | | sneq 4600 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β {π₯} = {π€}) |
56 | 55 | xpeq2d 5667 |
. . . . . . . . . . . . 13
β’ (π₯ = π€ β (π Γ {π₯}) = (π Γ {π€})) |
57 | 56 | sseq1d 3979 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β ((π Γ {π₯}) β π£ β (π Γ {π€}) β π£)) |
58 | 57 | elrab 3649 |
. . . . . . . . . . 11
β’ (π€ β {π₯ β π β£ (π Γ {π₯}) β π£} β (π€ β π β§ (π Γ {π€}) β π£)) |
59 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ βͺ (π
βΎt π) =
βͺ (π βΎt π) |
60 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ βͺ π
=
βͺ π
|
61 | | simplr 768 |
. . . . . . . . . . . . 13
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π βΎt π) β Comp) |
62 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β π
β (TopOnβπ)) |
63 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π
β (TopOnβπ)) |
64 | | topontop 22285 |
. . . . . . . . . . . . . 14
β’ (π
β (TopOnβπ) β π
β Top) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π
β Top) |
66 | | topontop 22285 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (TopOnβπ) β π β Top) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β π β Top) |
68 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β π
β Top) |
69 | | txtop 22943 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Top β§ π
β Top) β (π Γt π
) β Top) |
70 | 67, 68, 69 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π Γt π
) β Top) |
71 | 70 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π Γt π
) β Top) |
72 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π β V |
73 | | toponmax 22298 |
. . . . . . . . . . . . . . . . 17
β’ (π
β (TopOnβπ) β π β π
) |
74 | 63, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π β π
) |
75 | | xpexg 7688 |
. . . . . . . . . . . . . . . 16
β’ ((π β V β§ π β π
) β (π Γ π) β V) |
76 | 72, 74, 75 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π Γ π) β V) |
77 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β π£ β (π Γt π
)) |
78 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π£ β (π Γt π
)) |
79 | | elrestr 17318 |
. . . . . . . . . . . . . . 15
β’ (((π Γt π
) β Top β§ (π Γ π) β V β§ π£ β (π Γt π
)) β (π£ β© (π Γ π)) β ((π Γt π
) βΎt (π Γ π))) |
80 | 71, 76, 78, 79 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π£ β© (π Γ π)) β ((π Γt π
) βΎt (π Γ π))) |
81 | 67 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π β Top) |
82 | 72 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π β V) |
83 | | txrest 23005 |
. . . . . . . . . . . . . . . 16
β’ (((π β Top β§ π
β Top) β§ (π β V β§ π β π
)) β ((π Γt π
) βΎt (π Γ π)) = ((π βΎt π) Γt (π
βΎt π))) |
84 | 81, 65, 82, 74, 83 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β ((π Γt π
) βΎt (π Γ π)) = ((π βΎt π) Γt (π
βΎt π))) |
85 | | toponuni 22286 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β (TopOnβπ) β π = βͺ π
) |
86 | 63, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π = βͺ π
) |
87 | 86 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π
βΎt π) = (π
βΎt βͺ π
)) |
88 | 60 | restid 17323 |
. . . . . . . . . . . . . . . . . 18
β’ (π
β (TopOnβπ) β (π
βΎt βͺ π
) =
π
) |
89 | 63, 88 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π
βΎt βͺ π
) =
π
) |
90 | 87, 89 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π
βΎt π) = π
) |
91 | 90 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β ((π βΎt π) Γt (π
βΎt π)) = ((π βΎt π) Γt π
)) |
92 | 84, 91 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β ((π Γt π
) βΎt (π Γ π)) = ((π βΎt π) Γt π
)) |
93 | 80, 92 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π£ β© (π Γ π)) β ((π βΎt π) Γt π
)) |
94 | 23 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π β (TopOnβπ)) |
95 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π β π) |
96 | | resttopon 22535 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (TopOnβπ) β§ π β π) β (π βΎt π) β (TopOnβπ)) |
97 | 94, 95, 96 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π βΎt π) β (TopOnβπ)) |
98 | | toponuni 22286 |
. . . . . . . . . . . . . . . 16
β’ ((π βΎt π) β (TopOnβπ) β π = βͺ (π βΎt π)) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π = βͺ (π βΎt π)) |
100 | 99 | xpeq1d 5666 |
. . . . . . . . . . . . . 14
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π Γ {π€}) = (βͺ (π βΎt π) Γ {π€})) |
101 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π Γ {π€}) β π£) |
102 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π€ β π) |
103 | 102 | snssd 4773 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β {π€} β π) |
104 | | xpss2 5657 |
. . . . . . . . . . . . . . . 16
β’ ({π€} β π β (π Γ {π€}) β (π Γ π)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π Γ {π€}) β (π Γ π)) |
106 | 101, 105 | ssind 4196 |
. . . . . . . . . . . . . 14
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (π Γ {π€}) β (π£ β© (π Γ π))) |
107 | 100, 106 | eqsstrrd 3987 |
. . . . . . . . . . . . 13
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (βͺ
(π βΎt
π) Γ {π€}) β (π£ β© (π Γ π))) |
108 | 102, 86 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β π€ β βͺ π
) |
109 | 59, 60, 61, 65, 93, 107, 108 | txtube 23014 |
. . . . . . . . . . . 12
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β βπ β π
(π€ β π β§ (βͺ (π βΎt π) Γ π) β (π£ β© (π Γ π)))) |
110 | | toponss 22299 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β (TopOnβπ) β§ π β π
) β π β π) |
111 | 63, 110 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β π β π) |
112 | | ssrab 4034 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π₯ β π β£ (π Γ {π₯}) β π£} β (π β π β§ βπ₯ β π (π Γ {π₯}) β π£)) |
113 | 112 | baib 537 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (π β {π₯ β π β£ (π Γ {π₯}) β π£} β βπ₯ β π (π Γ {π₯}) β π£)) |
114 | 111, 113 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β (π β {π₯ β π β£ (π Γ {π₯}) β π£} β βπ₯ β π (π Γ {π₯}) β π£)) |
115 | | xpss2 5657 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (π Γ π) β (π Γ π)) |
116 | 111, 115 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β (π Γ π) β (π Γ π)) |
117 | 116 | biantrud 533 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β ((π Γ π) β π£ β ((π Γ π) β π£ β§ (π Γ π) β (π Γ π)))) |
118 | | iunid 5024 |
. . . . . . . . . . . . . . . . . . . 20
β’ βͺ π₯ β π {π₯} = π |
119 | 118 | xpeq2i 5664 |
. . . . . . . . . . . . . . . . . . 19
β’ (π Γ βͺ π₯ β π {π₯}) = (π Γ π) |
120 | | xpiundi 5706 |
. . . . . . . . . . . . . . . . . . 19
β’ (π Γ βͺ π₯ β π {π₯}) = βͺ
π₯ β π (π Γ {π₯}) |
121 | 119, 120 | eqtr3i 2763 |
. . . . . . . . . . . . . . . . . 18
β’ (π Γ π) = βͺ π₯ β π (π Γ {π₯}) |
122 | 121 | sseq1i 3976 |
. . . . . . . . . . . . . . . . 17
β’ ((π Γ π) β π£ β βͺ
π₯ β π (π Γ {π₯}) β π£) |
123 | | iunss 5009 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ π₯ β π (π Γ {π₯}) β π£ β βπ₯ β π (π Γ {π₯}) β π£) |
124 | 122, 123 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’ ((π Γ π) β π£ β βπ₯ β π (π Γ {π₯}) β π£) |
125 | | ssin 4194 |
. . . . . . . . . . . . . . . 16
β’ (((π Γ π) β π£ β§ (π Γ π) β (π Γ π)) β (π Γ π) β (π£ β© (π Γ π))) |
126 | 117, 124,
125 | 3bitr3g 313 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β (βπ₯ β π (π Γ {π₯}) β π£ β (π Γ π) β (π£ β© (π Γ π)))) |
127 | 99 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β π = βͺ (π βΎt π)) |
128 | 127 | xpeq1d 5666 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β (π Γ π) = (βͺ (π βΎt π) Γ π)) |
129 | 128 | sseq1d 3979 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β ((π Γ π) β (π£ β© (π Γ π)) β (βͺ
(π βΎt
π) Γ π) β (π£ β© (π Γ π)))) |
130 | 114, 126,
129 | 3bitrd 305 |
. . . . . . . . . . . . . 14
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β (π β {π₯ β π β£ (π Γ {π₯}) β π£} β (βͺ (π βΎt π) Γ π) β (π£ β© (π Γ π)))) |
131 | 130 | anbi2d 630 |
. . . . . . . . . . . . 13
β’
((((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β§ π β π
) β ((π€ β π β§ π β {π₯ β π β£ (π Γ {π₯}) β π£}) β (π€ β π β§ (βͺ (π βΎt π) Γ π) β (π£ β© (π Γ π))))) |
132 | 131 | rexbidva 3170 |
. . . . . . . . . . . 12
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β (βπ β π
(π€ β π β§ π β {π₯ β π β£ (π Γ {π₯}) β π£}) β βπ β π
(π€ β π β§ (βͺ (π βΎt π) Γ π) β (π£ β© (π Γ π))))) |
133 | 109, 132 | mpbird 257 |
. . . . . . . . . . 11
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ (π€ β π β§ (π Γ {π€}) β π£)) β βπ β π
(π€ β π β§ π β {π₯ β π β£ (π Γ {π₯}) β π£})) |
134 | 58, 133 | sylan2b 595 |
. . . . . . . . . 10
β’
(((((π
β
(TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β§ π€ β {π₯ β π β£ (π Γ {π₯}) β π£}) β βπ β π
(π€ β π β§ π β {π₯ β π β£ (π Γ {π₯}) β π£})) |
135 | 134 | ralrimiva 3140 |
. . . . . . . . 9
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β βπ€ β {π₯ β π β£ (π Γ {π₯}) β π£}βπ β π
(π€ β π β§ π β {π₯ β π β£ (π Γ {π₯}) β π£})) |
136 | | eltop2 22348 |
. . . . . . . . . 10
β’ (π
β Top β ({π₯ β π β£ (π Γ {π₯}) β π£} β π
β βπ€ β {π₯ β π β£ (π Γ {π₯}) β π£}βπ β π
(π€ β π β§ π β {π₯ β π β£ (π Γ {π₯}) β π£}))) |
137 | 14, 68, 136 | 3syl 18 |
. . . . . . . . 9
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β ({π₯ β π β£ (π Γ {π₯}) β π£} β π
β βπ€ β {π₯ β π β£ (π Γ {π₯}) β π£}βπ β π
(π€ β π β§ π β {π₯ β π β£ (π Γ {π₯}) β π£}))) |
138 | 135, 137 | mpbird 257 |
. . . . . . . 8
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β {π₯ β π β£ (π Γ {π₯}) β π£} β π
) |
139 | 54, 138 | eqeltrd 2834 |
. . . . . . 7
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β {π₯ β π β£ (π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£}} β π
) |
140 | | imaeq2 6013 |
. . . . . . . . 9
β’ (π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£} β (β‘πΉ β π§) = (β‘πΉ β {π β (π Cn (π Γt π
)) β£ (π β π) β π£})) |
141 | 7 | mptpreima 6194 |
. . . . . . . . 9
β’ (β‘πΉ β {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) = {π₯ β π β£ (π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£}} |
142 | 140, 141 | eqtrdi 2789 |
. . . . . . . 8
β’ (π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£} β (β‘πΉ β π§) = {π₯ β π β£ (π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£}}) |
143 | 142 | eleq1d 2819 |
. . . . . . 7
β’ (π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£} β ((β‘πΉ β π§) β π
β {π₯ β π β£ (π¦ β π β¦ β¨π¦, π₯β©) β {π β (π Cn (π Γt π
)) β£ (π β π) β π£}} β π
)) |
144 | 139, 143 | syl5ibrcom 247 |
. . . . . 6
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β§ (π βΎt π) β Comp) β (π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£} β (β‘πΉ β π§) β π
)) |
145 | 144 | expimpd 455 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π« βͺ π
β§ π£ β (π Γt π
))) β (((π βΎt π) β Comp β§ π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β (β‘πΉ β π§) β π
)) |
146 | 145 | rexlimdvva 3202 |
. . . 4
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (βπ β π« βͺ πβπ£ β (π Γt π
)((π βΎt π) β Comp β§ π§ = {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β (β‘πΉ β π§) β π
)) |
147 | 13, 146 | biimtrid 241 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π§ β ran (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β (β‘πΉ β π§) β π
)) |
148 | 147 | ralrimiv 3139 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β βπ§ β ran (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£})(β‘πΉ β π§) β π
) |
149 | | simpl 484 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β π
β (TopOnβπ)) |
150 | | ovex 7394 |
. . . . . 6
β’ (π Cn (π Γt π
)) β V |
151 | 150 | pwex 5339 |
. . . . 5
β’ π«
(π Cn (π Γt π
)) β V |
152 | 9, 10, 11 | xkotf 22959 |
. . . . . 6
β’ (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}):({π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp} Γ (π
Γt π
))βΆπ« (π Cn (π Γt π
)) |
153 | | frn 6679 |
. . . . . 6
β’ ((π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}):({π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp} Γ (π
Γt π
))βΆπ« (π Cn (π Γt π
)) β ran (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β π« (π Cn (π Γt π
))) |
154 | 152, 153 | ax-mp 5 |
. . . . 5
β’ ran
(π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β π« (π Cn (π Γt π
)) |
155 | 151, 154 | ssexi 5283 |
. . . 4
β’ ran
(π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β V |
156 | 155 | a1i 11 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ran (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£}) β V) |
157 | 9, 10, 11 | xkoval 22961 |
. . . 4
β’ ((π β Top β§ (π Γt π
) β Top) β ((π Γt π
) βko π) = (topGenβ(fiβran
(π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£})))) |
158 | 67, 70, 157 | syl2anc 585 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((π Γt π
) βko π) = (topGenβ(fiβran (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£})))) |
159 | | eqid 2733 |
. . . . 5
β’ ((π Γt π
) βko π) = ((π Γt π
) βko π) |
160 | 159 | xkotopon 22974 |
. . . 4
β’ ((π β Top β§ (π Γt π
) β Top) β ((π Γt π
) βko π) β (TopOnβ(π Cn (π Γt π
)))) |
161 | 67, 70, 160 | syl2anc 585 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((π Γt π
) βko π) β (TopOnβ(π Cn (π Γt π
)))) |
162 | 149, 156,
158, 161 | subbascn 22628 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (πΉ β (π
Cn ((π Γt π
) βko π)) β (πΉ:πβΆ(π Cn (π Γt π
)) β§ βπ§ β ran (π β {π€ β π« βͺ π
β£ (π
βΎt π€)
β Comp}, π£ β
(π Γt
π
) β¦ {π β (π Cn (π Γt π
)) β£ (π β π) β π£})(β‘πΉ β π§) β π
))) |
163 | 8, 148, 162 | mpbir2and 712 |
1
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β πΉ β (π
Cn ((π Γt π
) βko π))) |