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