Step | Hyp | Ref
| Expression |
1 | | xkofvcn.2 |
. 2
β’ πΉ = (π β (π
Cn π), π₯ β π β¦ (πβπ₯)) |
2 | | nllytop 22847 |
. . . 4
β’ (π
β π-Locally Comp
β π
β
Top) |
3 | | eqid 2733 |
. . . . 5
β’ (π βko π
) = (π βko π
) |
4 | 3 | xkotopon 22974 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π βko π
) β (TopOnβ(π
Cn π))) |
5 | 2, 4 | sylan 581 |
. . 3
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π βko
π
) β
(TopOnβ(π
Cn π))) |
6 | 2 | adantr 482 |
. . . 4
β’ ((π
β π-Locally Comp
β§ π β Top) β
π
β
Top) |
7 | | xkofvcn.1 |
. . . . 5
β’ π = βͺ
π
|
8 | 7 | toptopon 22289 |
. . . 4
β’ (π
β Top β π
β (TopOnβπ)) |
9 | 6, 8 | sylib 217 |
. . 3
β’ ((π
β π-Locally Comp
β§ π β Top) β
π
β (TopOnβπ)) |
10 | 5, 9 | cnmpt1st 23042 |
. . . 4
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π β (π
Cn π), π₯ β π β¦ π) β (((π βko π
) Γt π
) Cn (π βko π
))) |
11 | 5, 9 | cnmpt2nd 23043 |
. . . . 5
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π β (π
Cn π), π₯ β π β¦ π₯) β (((π βko π
) Γt π
) Cn π
)) |
12 | | 1on 8428 |
. . . . . . 7
β’
1o β On |
13 | | distopon 22370 |
. . . . . . 7
β’
(1o β On β π« 1o β
(TopOnβ1o)) |
14 | 12, 13 | mp1i 13 |
. . . . . 6
β’ ((π
β π-Locally Comp
β§ π β Top) β
π« 1o β (TopOnβ1o)) |
15 | | xkoccn 22993 |
. . . . . 6
β’
((π« 1o β (TopOnβ1o) β§ π
β (TopOnβπ)) β (π¦ β π β¦ (1o Γ {π¦})) β (π
Cn (π
βko π«
1o))) |
16 | 14, 9, 15 | syl2anc 585 |
. . . . 5
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π¦ β π β¦ (1o Γ {π¦})) β (π
Cn (π
βko π«
1o))) |
17 | | sneq 4600 |
. . . . . 6
β’ (π¦ = π₯ β {π¦} = {π₯}) |
18 | 17 | xpeq2d 5667 |
. . . . 5
β’ (π¦ = π₯ β (1o Γ {π¦}) = (1o Γ
{π₯})) |
19 | 5, 9, 11, 9, 16, 18 | cnmpt21 23045 |
. . . 4
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π β (π
Cn π), π₯ β π β¦ (1o Γ {π₯})) β (((π βko π
) Γt π
) Cn (π
βko π«
1o))) |
20 | | distop 22368 |
. . . . . 6
β’
(1o β On β π« 1o β
Top) |
21 | 12, 20 | mp1i 13 |
. . . . 5
β’ ((π
β π-Locally Comp
β§ π β Top) β
π« 1o β Top) |
22 | | eqid 2733 |
. . . . . 6
β’ (π
βko π«
1o) = (π
βko π« 1o) |
23 | 22 | xkotopon 22974 |
. . . . 5
β’
((π« 1o β Top β§ π
β Top) β (π
βko π«
1o) β (TopOnβ(π« 1o Cn π
))) |
24 | 21, 6, 23 | syl2anc 585 |
. . . 4
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π
βko
π« 1o) β (TopOnβ(π« 1o Cn π
))) |
25 | | simpl 484 |
. . . . 5
β’ ((π
β π-Locally Comp
β§ π β Top) β
π
β π-Locally
Comp) |
26 | | simpr 486 |
. . . . 5
β’ ((π
β π-Locally Comp
β§ π β Top) β
π β
Top) |
27 | | eqid 2733 |
. . . . . 6
β’ (π β (π
Cn π), β β (π« 1o Cn π
) β¦ (π β β)) = (π β (π
Cn π), β β (π« 1o Cn π
) β¦ (π β β)) |
28 | 27 | xkococn 23034 |
. . . . 5
β’
((π« 1o β Top β§ π
β π-Locally Comp β§ π β Top) β (π β (π
Cn π), β β (π« 1o Cn π
) β¦ (π β β)) β (((π βko π
) Γt (π
βko π«
1o)) Cn (π
βko π« 1o))) |
29 | 21, 25, 26, 28 | syl3anc 1372 |
. . . 4
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π β (π
Cn π), β β (π« 1o Cn π
) β¦ (π β β)) β (((π βko π
) Γt (π
βko π«
1o)) Cn (π
βko π« 1o))) |
30 | | coeq1 5817 |
. . . . 5
β’ (π = π β (π β β) = (π β β)) |
31 | | coeq2 5818 |
. . . . 5
β’ (β = (1o Γ {π₯}) β (π β β) = (π β (1o Γ {π₯}))) |
32 | 30, 31 | sylan9eq 2793 |
. . . 4
β’ ((π = π β§ β = (1o Γ {π₯})) β (π β β) = (π β (1o Γ {π₯}))) |
33 | 5, 9, 10, 19, 5, 24, 29, 32 | cnmpt22 23048 |
. . 3
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π β (π
Cn π), π₯ β π β¦ (π β (1o Γ {π₯}))) β (((π βko π
) Γt π
) Cn (π βko π«
1o))) |
34 | | eqid 2733 |
. . . . 5
β’ (π βko π«
1o) = (π
βko π« 1o) |
35 | 34 | xkotopon 22974 |
. . . 4
β’
((π« 1o β Top β§ π β Top) β (π βko π«
1o) β (TopOnβ(π« 1o Cn π))) |
36 | 21, 26, 35 | syl2anc 585 |
. . 3
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π βko
π« 1o) β (TopOnβ(π« 1o Cn π))) |
37 | | 0lt1o 8454 |
. . . . 5
β’ β
β 1o |
38 | 37 | a1i 11 |
. . . 4
β’ ((π
β π-Locally Comp
β§ π β Top) β
β
β 1o) |
39 | | unipw 5411 |
. . . . . 6
β’ βͺ π« 1o = 1o |
40 | 39 | eqcomi 2742 |
. . . . 5
β’
1o = βͺ π«
1o |
41 | 40 | xkopjcn 23030 |
. . . 4
β’
((π« 1o β Top β§ π β Top β§ β
β
1o) β (π
β (π« 1o Cn π) β¦ (πββ
)) β ((π βko π«
1o) Cn π)) |
42 | 21, 26, 38, 41 | syl3anc 1372 |
. . 3
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π β (π«
1o Cn π) β¦
(πββ
)) β
((π βko
π« 1o) Cn π)) |
43 | | fveq1 6845 |
. . . 4
β’ (π = (π β (1o Γ {π₯})) β (πββ
) = ((π β (1o Γ {π₯}))ββ
)) |
44 | | vex 3451 |
. . . . . . 7
β’ π₯ β V |
45 | 44 | fconst 6732 |
. . . . . 6
β’
(1o Γ {π₯}):1oβΆ{π₯} |
46 | | fvco3 6944 |
. . . . . 6
β’
(((1o Γ {π₯}):1oβΆ{π₯} β§ β
β 1o) β
((π β (1o
Γ {π₯}))ββ
) = (πβ((1o Γ {π₯})ββ
))) |
47 | 45, 37, 46 | mp2an 691 |
. . . . 5
β’ ((π β (1o Γ
{π₯}))ββ
) =
(πβ((1o
Γ {π₯})ββ
)) |
48 | 44 | fvconst2 7157 |
. . . . . . 7
β’ (β
β 1o β ((1o Γ {π₯})ββ
) = π₯) |
49 | 37, 48 | ax-mp 5 |
. . . . . 6
β’
((1o Γ {π₯})ββ
) = π₯ |
50 | 49 | fveq2i 6849 |
. . . . 5
β’ (πβ((1o Γ
{π₯})ββ
)) =
(πβπ₯) |
51 | 47, 50 | eqtri 2761 |
. . . 4
β’ ((π β (1o Γ
{π₯}))ββ
) =
(πβπ₯) |
52 | 43, 51 | eqtrdi 2789 |
. . 3
β’ (π = (π β (1o Γ {π₯})) β (πββ
) = (πβπ₯)) |
53 | 5, 9, 33, 36, 42, 52 | cnmpt21 23045 |
. 2
β’ ((π
β π-Locally Comp
β§ π β Top) β
(π β (π
Cn π), π₯ β π β¦ (πβπ₯)) β (((π βko π
) Γt π
) Cn π)) |
54 | 1, 53 | eqeltrid 2838 |
1
β’ ((π
β π-Locally Comp
β§ π β Top) β
πΉ β (((π βko π
) Γt π
) Cn π)) |