Step | Hyp | Ref
| Expression |
1 | | cnmptkk.k |
. . . . . . 7
β’ (π β πΎ β (TopOnβπ)) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β πΎ β (TopOnβπ)) |
3 | | cnmptkk.l |
. . . . . . 7
β’ (π β πΏ β (TopOnβπ)) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β πΏ β (TopOnβπ)) |
5 | | cnmptkk.j |
. . . . . . . 8
β’ (π β π½ β (TopOnβπ)) |
6 | | topontop 22285 |
. . . . . . . . . 10
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
7 | 1, 6 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ β Top) |
8 | | cnmptkk.n |
. . . . . . . . . 10
β’ (π β πΏ β π-Locally
Comp) |
9 | | nllytop 22847 |
. . . . . . . . . 10
β’ (πΏ β π-Locally Comp
β πΏ β
Top) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β πΏ β Top) |
11 | | eqid 2733 |
. . . . . . . . . 10
β’ (πΏ βko πΎ) = (πΏ βko πΎ) |
12 | 11 | xkotopon 22974 |
. . . . . . . . 9
β’ ((πΎ β Top β§ πΏ β Top) β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
13 | 7, 10, 12 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
14 | | cnmptkk.a |
. . . . . . . 8
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) |
15 | | cnf2 22623 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ)) β§ (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
16 | 5, 13, 14, 15 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
17 | 16 | fvmptelcdm 7065 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) |
18 | | cnf2 22623 |
. . . . . 6
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnβπ) β§ (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) β (π¦ β π β¦ π΄):πβΆπ) |
19 | 2, 4, 17, 18 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄):πβΆπ) |
20 | | eqid 2733 |
. . . . . 6
β’ (π¦ β π β¦ π΄) = (π¦ β π β¦ π΄) |
21 | 20 | fmpt 7062 |
. . . . 5
β’
(βπ¦ β
π π΄ β π β (π¦ β π β¦ π΄):πβΆπ) |
22 | 19, 21 | sylibr 233 |
. . . 4
β’ ((π β§ π₯ β π) β βπ¦ β π π΄ β π) |
23 | | eqidd 2734 |
. . . 4
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄) = (π¦ β π β¦ π΄)) |
24 | | eqidd 2734 |
. . . 4
β’ ((π β§ π₯ β π) β (π§ β π β¦ π΅) = (π§ β π β¦ π΅)) |
25 | | cnmptkk.c |
. . . 4
β’ (π§ = π΄ β π΅ = πΆ) |
26 | 22, 23, 24, 25 | fmptcof 7080 |
. . 3
β’ ((π β§ π₯ β π) β ((π§ β π β¦ π΅) β (π¦ β π β¦ π΄)) = (π¦ β π β¦ πΆ)) |
27 | 26 | mpteq2dva 5209 |
. 2
β’ (π β (π₯ β π β¦ ((π§ β π β¦ π΅) β (π¦ β π β¦ π΄))) = (π₯ β π β¦ (π¦ β π β¦ πΆ))) |
28 | | cnmptkk.b |
. . 3
β’ (π β (π₯ β π β¦ (π§ β π β¦ π΅)) β (π½ Cn (π βko πΏ))) |
29 | | cnmptkk.m |
. . . . 5
β’ (π β π β (TopOnβπ)) |
30 | | topontop 22285 |
. . . . 5
β’ (π β (TopOnβπ) β π β Top) |
31 | 29, 30 | syl 17 |
. . . 4
β’ (π β π β Top) |
32 | | eqid 2733 |
. . . . 5
β’ (π βko πΏ) = (π βko πΏ) |
33 | 32 | xkotopon 22974 |
. . . 4
β’ ((πΏ β Top β§ π β Top) β (π βko πΏ) β (TopOnβ(πΏ Cn π))) |
34 | 10, 31, 33 | syl2anc 585 |
. . 3
β’ (π β (π βko πΏ) β (TopOnβ(πΏ Cn π))) |
35 | | eqid 2733 |
. . . . 5
β’ (π β (πΏ Cn π), π β (πΎ Cn πΏ) β¦ (π β π)) = (π β (πΏ Cn π), π β (πΎ Cn πΏ) β¦ (π β π)) |
36 | 35 | xkococn 23034 |
. . . 4
β’ ((πΎ β Top β§ πΏ β π-Locally Comp
β§ π β Top) β
(π β (πΏ Cn π), π β (πΎ Cn πΏ) β¦ (π β π)) β (((π βko πΏ) Γt (πΏ βko πΎ)) Cn (π βko πΎ))) |
37 | 7, 8, 31, 36 | syl3anc 1372 |
. . 3
β’ (π β (π β (πΏ Cn π), π β (πΎ Cn πΏ) β¦ (π β π)) β (((π βko πΏ) Γt (πΏ βko πΎ)) Cn (π βko πΎ))) |
38 | | coeq1 5817 |
. . . 4
β’ (π = (π§ β π β¦ π΅) β (π β π) = ((π§ β π β¦ π΅) β π)) |
39 | | coeq2 5818 |
. . . 4
β’ (π = (π¦ β π β¦ π΄) β ((π§ β π β¦ π΅) β π) = ((π§ β π β¦ π΅) β (π¦ β π β¦ π΄))) |
40 | 38, 39 | sylan9eq 2793 |
. . 3
β’ ((π = (π§ β π β¦ π΅) β§ π = (π¦ β π β¦ π΄)) β (π β π) = ((π§ β π β¦ π΅) β (π¦ β π β¦ π΄))) |
41 | 5, 28, 14, 34, 13, 37, 40 | cnmpt12 23041 |
. 2
β’ (π β (π₯ β π β¦ ((π§ β π β¦ π΅) β (π¦ β π β¦ π΄))) β (π½ Cn (π βko πΎ))) |
42 | 27, 41 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ (π¦ β π β¦ πΆ)) β (π½ Cn (π βko πΎ))) |