Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’ (π βko π
) = (π βko π
) |
2 | 1 | xkotopon 23104 |
. . . . 5
β’ ((π
β Top β§ π β Top) β (π βko π
) β (TopOnβ(π
Cn π))) |
3 | 2 | 3adant3 1133 |
. . . 4
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π βko π
) β (TopOnβ(π
Cn π))) |
4 | | xkopjcn.1 |
. . . . . . . . 9
β’ π = βͺ
π
|
5 | 4 | topopn 22408 |
. . . . . . . 8
β’ (π
β Top β π β π
) |
6 | 5 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π
β Top β§ π β Top β§ π΄ β π) β π β π
) |
7 | | fconst6g 6781 |
. . . . . . . 8
β’ (π β Top β (π Γ {π}):πβΆTop) |
8 | 7 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π Γ {π}):πβΆTop) |
9 | | pttop 23086 |
. . . . . . 7
β’ ((π β π
β§ (π Γ {π}):πβΆTop) β
(βtβ(π Γ {π})) β Top) |
10 | 6, 8, 9 | syl2anc 585 |
. . . . . 6
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (βtβ(π Γ {π})) β Top) |
11 | | eqid 2733 |
. . . . . . . . . 10
β’ βͺ π =
βͺ π |
12 | 4, 11 | cnf 22750 |
. . . . . . . . 9
β’ (π β (π
Cn π) β π:πβΆβͺ π) |
13 | | uniexg 7730 |
. . . . . . . . . . 11
β’ (π β Top β βͺ π
β V) |
14 | 13 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((π
β Top β§ π β Top β§ π΄ β π) β βͺ π β V) |
15 | 14, 6 | elmapd 8834 |
. . . . . . . . 9
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π β (βͺ π βm π) β π:πβΆβͺ π)) |
16 | 12, 15 | imbitrrid 245 |
. . . . . . . 8
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π β (π
Cn π) β π β (βͺ π βm π))) |
17 | 16 | ssrdv 3989 |
. . . . . . 7
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π
Cn π) β (βͺ
π βm π)) |
18 | | simp2 1138 |
. . . . . . . 8
β’ ((π
β Top β§ π β Top β§ π΄ β π) β π β Top) |
19 | | eqid 2733 |
. . . . . . . . 9
β’
(βtβ(π Γ {π})) = (βtβ(π Γ {π})) |
20 | 19, 11 | ptuniconst 23102 |
. . . . . . . 8
β’ ((π β π
β§ π β Top) β (βͺ π
βm π) =
βͺ (βtβ(π Γ {π}))) |
21 | 6, 18, 20 | syl2anc 585 |
. . . . . . 7
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (βͺ π βm π) = βͺ
(βtβ(π Γ {π}))) |
22 | 17, 21 | sseqtrd 4023 |
. . . . . 6
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π
Cn π) β βͺ
(βtβ(π Γ {π}))) |
23 | | eqid 2733 |
. . . . . . 7
β’ βͺ (βtβ(π Γ {π})) = βͺ
(βtβ(π Γ {π})) |
24 | 23 | restuni 22666 |
. . . . . 6
β’
(((βtβ(π Γ {π})) β Top β§ (π
Cn π) β βͺ
(βtβ(π Γ {π}))) β (π
Cn π) = βͺ
((βtβ(π Γ {π})) βΎt (π
Cn π))) |
25 | 10, 22, 24 | syl2anc 585 |
. . . . 5
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π
Cn π) = βͺ
((βtβ(π Γ {π})) βΎt (π
Cn π))) |
26 | 25 | fveq2d 6896 |
. . . 4
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (TopOnβ(π
Cn π)) = (TopOnββͺ ((βtβ(π Γ {π})) βΎt (π
Cn π)))) |
27 | 3, 26 | eleqtrd 2836 |
. . 3
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π βko π
) β (TopOnββͺ ((βtβ(π Γ {π})) βΎt (π
Cn π)))) |
28 | 4, 19 | xkoptsub 23158 |
. . . 4
β’ ((π
β Top β§ π β Top) β
((βtβ(π Γ {π})) βΎt (π
Cn π)) β (π βko π
)) |
29 | 28 | 3adant3 1133 |
. . 3
β’ ((π
β Top β§ π β Top β§ π΄ β π) β ((βtβ(π Γ {π})) βΎt (π
Cn π)) β (π βko π
)) |
30 | | eqid 2733 |
. . . 4
β’ βͺ ((βtβ(π Γ {π})) βΎt (π
Cn π)) = βͺ
((βtβ(π Γ {π})) βΎt (π
Cn π)) |
31 | 30 | cnss1 22780 |
. . 3
β’ (((π βko π
) β (TopOnββͺ ((βtβ(π Γ {π})) βΎt (π
Cn π))) β§ ((βtβ(π Γ {π})) βΎt (π
Cn π)) β (π βko π
)) β (((βtβ(π Γ {π})) βΎt (π
Cn π)) Cn π) β ((π βko π
) Cn π)) |
32 | 27, 29, 31 | syl2anc 585 |
. 2
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (((βtβ(π Γ {π})) βΎt (π
Cn π)) Cn π) β ((π βko π
) Cn π)) |
33 | 22 | resmptd 6041 |
. . 3
β’ ((π
β Top β§ π β Top β§ π΄ β π) β ((π β βͺ
(βtβ(π Γ {π})) β¦ (πβπ΄)) βΎ (π
Cn π)) = (π β (π
Cn π) β¦ (πβπ΄))) |
34 | | simp3 1139 |
. . . . . 6
β’ ((π
β Top β§ π β Top β§ π΄ β π) β π΄ β π) |
35 | 23, 19 | ptpjcn 23115 |
. . . . . 6
β’ ((π β π
β§ (π Γ {π}):πβΆTop β§ π΄ β π) β (π β βͺ
(βtβ(π Γ {π})) β¦ (πβπ΄)) β ((βtβ(π Γ {π})) Cn ((π Γ {π})βπ΄))) |
36 | 6, 8, 34, 35 | syl3anc 1372 |
. . . . 5
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π β βͺ
(βtβ(π Γ {π})) β¦ (πβπ΄)) β ((βtβ(π Γ {π})) Cn ((π Γ {π})βπ΄))) |
37 | | fvconst2g 7203 |
. . . . . . 7
β’ ((π β Top β§ π΄ β π) β ((π Γ {π})βπ΄) = π) |
38 | 37 | 3adant1 1131 |
. . . . . 6
β’ ((π
β Top β§ π β Top β§ π΄ β π) β ((π Γ {π})βπ΄) = π) |
39 | 38 | oveq2d 7425 |
. . . . 5
β’ ((π
β Top β§ π β Top β§ π΄ β π) β ((βtβ(π Γ {π})) Cn ((π Γ {π})βπ΄)) = ((βtβ(π Γ {π})) Cn π)) |
40 | 36, 39 | eleqtrd 2836 |
. . . 4
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π β βͺ
(βtβ(π Γ {π})) β¦ (πβπ΄)) β ((βtβ(π Γ {π})) Cn π)) |
41 | 23 | cnrest 22789 |
. . . 4
β’ (((π β βͺ (βtβ(π Γ {π})) β¦ (πβπ΄)) β ((βtβ(π Γ {π})) Cn π) β§ (π
Cn π) β βͺ
(βtβ(π Γ {π}))) β ((π β βͺ
(βtβ(π Γ {π})) β¦ (πβπ΄)) βΎ (π
Cn π)) β (((βtβ(π Γ {π})) βΎt (π
Cn π)) Cn π)) |
42 | 40, 22, 41 | syl2anc 585 |
. . 3
β’ ((π
β Top β§ π β Top β§ π΄ β π) β ((π β βͺ
(βtβ(π Γ {π})) β¦ (πβπ΄)) βΎ (π
Cn π)) β (((βtβ(π Γ {π})) βΎt (π
Cn π)) Cn π)) |
43 | 33, 42 | eqeltrrd 2835 |
. 2
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π β (π
Cn π) β¦ (πβπ΄)) β (((βtβ(π Γ {π})) βΎt (π
Cn π)) Cn π)) |
44 | 32, 43 | sseldd 3984 |
1
β’ ((π
β Top β§ π β Top β§ π΄ β π) β (π β (π
Cn π) β¦ (πβπ΄)) β ((π βko π
) Cn π)) |