Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’ (π¦ β π β¦ π΄) = (π¦ β π β¦ π΄) |
2 | | cnmptkp.c |
. . . 4
β’ (π¦ = π΅ β π΄ = πΆ) |
3 | | cnmptkp.b |
. . . . 5
β’ (π β π΅ β π) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β π) |
5 | 2 | eleq1d 2819 |
. . . . 5
β’ (π¦ = π΅ β (π΄ β βͺ πΏ β πΆ β βͺ πΏ)) |
6 | | cnmptk1.k |
. . . . . . . 8
β’ (π β πΎ β (TopOnβπ)) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β πΎ β (TopOnβπ)) |
8 | | cnmptk1.l |
. . . . . . . . . 10
β’ (π β πΏ β (TopOnβπ)) |
9 | | topontop 22285 |
. . . . . . . . . 10
β’ (πΏ β (TopOnβπ) β πΏ β Top) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β πΏ β Top) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β πΏ β Top) |
12 | | toptopon2 22290 |
. . . . . . . 8
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
13 | 11, 12 | sylib 217 |
. . . . . . 7
β’ ((π β§ π₯ β π) β πΏ β (TopOnββͺ πΏ)) |
14 | | cnmptk1.j |
. . . . . . . . 9
β’ (π β π½ β (TopOnβπ)) |
15 | | topontop 22285 |
. . . . . . . . . . 11
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
16 | 6, 15 | syl 17 |
. . . . . . . . . 10
β’ (π β πΎ β Top) |
17 | | eqid 2733 |
. . . . . . . . . . 11
β’ (πΏ βko πΎ) = (πΏ βko πΎ) |
18 | 17 | xkotopon 22974 |
. . . . . . . . . 10
β’ ((πΎ β Top β§ πΏ β Top) β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
19 | 16, 10, 18 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
20 | | cnmptkp.a |
. . . . . . . . 9
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) |
21 | | cnf2 22623 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ)) β§ (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
22 | 14, 19, 20, 21 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
23 | 22 | fvmptelcdm 7065 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) |
24 | | cnf2 22623 |
. . . . . . 7
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnββͺ πΏ)
β§ (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) β (π¦ β π β¦ π΄):πβΆβͺ πΏ) |
25 | 7, 13, 23, 24 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄):πβΆβͺ πΏ) |
26 | 1 | fmpt 7062 |
. . . . . 6
β’
(βπ¦ β
π π΄ β βͺ πΏ β (π¦ β π β¦ π΄):πβΆβͺ πΏ) |
27 | 25, 26 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β π) β βπ¦ β π π΄ β βͺ πΏ) |
28 | 5, 27, 4 | rspcdva 3584 |
. . . 4
β’ ((π β§ π₯ β π) β πΆ β βͺ πΏ) |
29 | 1, 2, 4, 28 | fvmptd3 6975 |
. . 3
β’ ((π β§ π₯ β π) β ((π¦ β π β¦ π΄)βπ΅) = πΆ) |
30 | 29 | mpteq2dva 5209 |
. 2
β’ (π β (π₯ β π β¦ ((π¦ β π β¦ π΄)βπ΅)) = (π₯ β π β¦ πΆ)) |
31 | | toponuni 22286 |
. . . . . 6
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
32 | 6, 31 | syl 17 |
. . . . 5
β’ (π β π = βͺ πΎ) |
33 | 3, 32 | eleqtrd 2836 |
. . . 4
β’ (π β π΅ β βͺ πΎ) |
34 | | eqid 2733 |
. . . . 5
β’ βͺ πΎ =
βͺ πΎ |
35 | 34 | xkopjcn 23030 |
. . . 4
β’ ((πΎ β Top β§ πΏ β Top β§ π΅ β βͺ πΎ)
β (π€ β (πΎ Cn πΏ) β¦ (π€βπ΅)) β ((πΏ βko πΎ) Cn πΏ)) |
36 | 16, 10, 33, 35 | syl3anc 1372 |
. . 3
β’ (π β (π€ β (πΎ Cn πΏ) β¦ (π€βπ΅)) β ((πΏ βko πΎ) Cn πΏ)) |
37 | | fveq1 6845 |
. . 3
β’ (π€ = (π¦ β π β¦ π΄) β (π€βπ΅) = ((π¦ β π β¦ π΄)βπ΅)) |
38 | 14, 20, 19, 36, 37 | cnmpt11 23037 |
. 2
β’ (π β (π₯ β π β¦ ((π¦ β π β¦ π΄)βπ΅)) β (π½ Cn πΏ)) |
39 | 30, 38 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) |