Step | Hyp | Ref
| Expression |
1 | | cnmptk1.j |
. . . . . . 7
β’ (π β π½ β (TopOnβπ)) |
2 | | cnmptk1.l |
. . . . . . 7
β’ (π β πΏ β (TopOnβπ)) |
3 | | cnmpt1k.a |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΏ)) |
4 | | cnf2 22623 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΏ β (TopOnβπ) β§ (π₯ β π β¦ π΄) β (π½ Cn πΏ)) β (π₯ β π β¦ π΄):πβΆπ) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. . . . . 6
β’ (π β (π₯ β π β¦ π΄):πβΆπ) |
6 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
7 | 6 | fmpt 7062 |
. . . . . 6
β’
(βπ₯ β
π π΄ β π β (π₯ β π β¦ π΄):πβΆπ) |
8 | 5, 7 | sylibr 233 |
. . . . 5
β’ (π β βπ₯ β π π΄ β π) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β π) β βπ₯ β π π΄ β π) |
10 | | eqidd 2734 |
. . . 4
β’ ((π β§ π¦ β π) β (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄)) |
11 | | eqidd 2734 |
. . . 4
β’ ((π β§ π¦ β π) β (π§ β π β¦ π΅) = (π§ β π β¦ π΅)) |
12 | | cnmpt1k.c |
. . . 4
β’ (π§ = π΄ β π΅ = πΆ) |
13 | 9, 10, 11, 12 | fmptcof 7080 |
. . 3
β’ ((π β§ π¦ β π) β ((π§ β π β¦ π΅) β (π₯ β π β¦ π΄)) = (π₯ β π β¦ πΆ)) |
14 | 13 | mpteq2dva 5209 |
. 2
β’ (π β (π¦ β π β¦ ((π§ β π β¦ π΅) β (π₯ β π β¦ π΄))) = (π¦ β π β¦ (π₯ β π β¦ πΆ))) |
15 | | cnmptk1.k |
. . 3
β’ (π β πΎ β (TopOnβπ)) |
16 | | cnmpt1k.b |
. . 3
β’ (π β (π¦ β π β¦ (π§ β π β¦ π΅)) β (πΎ Cn (π βko πΏ))) |
17 | | topontop 22285 |
. . . . 5
β’ (πΏ β (TopOnβπ) β πΏ β Top) |
18 | 2, 17 | syl 17 |
. . . 4
β’ (π β πΏ β Top) |
19 | | cnmpt1k.m |
. . . . 5
β’ (π β π β (TopOnβπ)) |
20 | | topontop 22285 |
. . . . 5
β’ (π β (TopOnβπ) β π β Top) |
21 | 19, 20 | syl 17 |
. . . 4
β’ (π β π β Top) |
22 | | eqid 2733 |
. . . . 5
β’ (π βko πΏ) = (π βko πΏ) |
23 | 22 | xkotopon 22974 |
. . . 4
β’ ((πΏ β Top β§ π β Top) β (π βko πΏ) β (TopOnβ(πΏ Cn π))) |
24 | 18, 21, 23 | syl2anc 585 |
. . 3
β’ (π β (π βko πΏ) β (TopOnβ(πΏ Cn π))) |
25 | 21, 3 | xkoco1cn 23031 |
. . 3
β’ (π β (π€ β (πΏ Cn π) β¦ (π€ β (π₯ β π β¦ π΄))) β ((π βko πΏ) Cn (π βko π½))) |
26 | | coeq1 5817 |
. . 3
β’ (π€ = (π§ β π β¦ π΅) β (π€ β (π₯ β π β¦ π΄)) = ((π§ β π β¦ π΅) β (π₯ β π β¦ π΄))) |
27 | 15, 16, 24, 25, 26 | cnmpt11 23037 |
. 2
β’ (π β (π¦ β π β¦ ((π§ β π β¦ π΅) β (π₯ β π β¦ π΄))) β (πΎ Cn (π βko π½))) |
28 | 14, 27 | eqeltrrd 2835 |
1
β’ (π β (π¦ β π β¦ (π₯ β π β¦ πΆ)) β (πΎ Cn (π βko π½))) |