Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’ (π¦ β π β¦ π΄) = (π¦ β π β¦ π΄) |
2 | | cnmptk1p.c |
. . . 4
β’ (π¦ = π΅ β π΄ = πΆ) |
3 | | cnmptk1p.j |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
4 | | cnmptk1p.k |
. . . . . 6
β’ (π β πΎ β (TopOnβπ)) |
5 | | cnmptk1p.b |
. . . . . 6
β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) |
6 | | cnf2 22623 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β (π₯ β π β¦ π΅):πβΆπ) |
7 | 3, 4, 5, 6 | syl3anc 1372 |
. . . . 5
β’ (π β (π₯ β π β¦ π΅):πβΆπ) |
8 | 7 | fvmptelcdm 7065 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β π) |
9 | 2 | eleq1d 2819 |
. . . . 5
β’ (π¦ = π΅ β (π΄ β π β πΆ β π)) |
10 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β πΎ β (TopOnβπ)) |
11 | | cnmptk1p.l |
. . . . . . . 8
β’ (π β πΏ β (TopOnβπ)) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β πΏ β (TopOnβπ)) |
13 | | cnmptk1p.n |
. . . . . . . . . . 11
β’ (π β πΎ β π-Locally
Comp) |
14 | | nllytop 22847 |
. . . . . . . . . . 11
β’ (πΎ β π-Locally Comp
β πΎ β
Top) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
β’ (π β πΎ β Top) |
16 | | topontop 22285 |
. . . . . . . . . . 11
β’ (πΏ β (TopOnβπ) β πΏ β Top) |
17 | 11, 16 | syl 17 |
. . . . . . . . . 10
β’ (π β πΏ β Top) |
18 | | eqid 2733 |
. . . . . . . . . . 11
β’ (πΏ βko πΎ) = (πΏ βko πΎ) |
19 | 18 | xkotopon 22974 |
. . . . . . . . . 10
β’ ((πΎ β Top β§ πΏ β Top) β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
20 | 15, 17, 19 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
21 | | cnmptk1p.a |
. . . . . . . . 9
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) |
22 | | cnf2 22623 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ)) β§ (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
23 | 3, 20, 21, 22 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
24 | 23 | fvmptelcdm 7065 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) |
25 | | cnf2 22623 |
. . . . . . 7
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnβπ) β§ (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) β (π¦ β π β¦ π΄):πβΆπ) |
26 | 10, 12, 24, 25 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄):πβΆπ) |
27 | 1 | fmpt 7062 |
. . . . . 6
β’
(βπ¦ β
π π΄ β π β (π¦ β π β¦ π΄):πβΆπ) |
28 | 26, 27 | sylibr 233 |
. . . . 5
β’ ((π β§ π₯ β π) β βπ¦ β π π΄ β π) |
29 | 9, 28, 8 | rspcdva 3584 |
. . . 4
β’ ((π β§ π₯ β π) β πΆ β π) |
30 | 1, 2, 8, 29 | fvmptd3 6975 |
. . 3
β’ ((π β§ π₯ β π) β ((π¦ β π β¦ π΄)βπ΅) = πΆ) |
31 | 30 | mpteq2dva 5209 |
. 2
β’ (π β (π₯ β π β¦ ((π¦ β π β¦ π΄)βπ΅)) = (π₯ β π β¦ πΆ)) |
32 | | eqid 2733 |
. . . . 5
β’ (πΎ Cn πΏ) = (πΎ Cn πΏ) |
33 | | toponuni 22286 |
. . . . . 6
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
34 | 4, 33 | syl 17 |
. . . . 5
β’ (π β π = βͺ πΎ) |
35 | | mpoeq12 7434 |
. . . . 5
β’ (((πΎ Cn πΏ) = (πΎ Cn πΏ) β§ π = βͺ πΎ) β (π β (πΎ Cn πΏ), π§ β π β¦ (πβπ§)) = (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§))) |
36 | 32, 34, 35 | sylancr 588 |
. . . 4
β’ (π β (π β (πΎ Cn πΏ), π§ β π β¦ (πβπ§)) = (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§))) |
37 | | eqid 2733 |
. . . . . 6
β’ βͺ πΎ =
βͺ πΎ |
38 | | eqid 2733 |
. . . . . 6
β’ (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) = (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) |
39 | 37, 38 | xkofvcn 23058 |
. . . . 5
β’ ((πΎ β π-Locally Comp
β§ πΏ β Top) β
(π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) β (((πΏ βko πΎ) Γt πΎ) Cn πΏ)) |
40 | 13, 17, 39 | syl2anc 585 |
. . . 4
β’ (π β (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) β (((πΏ βko πΎ) Γt πΎ) Cn πΏ)) |
41 | 36, 40 | eqeltrd 2834 |
. . 3
β’ (π β (π β (πΎ Cn πΏ), π§ β π β¦ (πβπ§)) β (((πΏ βko πΎ) Γt πΎ) Cn πΏ)) |
42 | | fveq1 6845 |
. . . 4
β’ (π = (π¦ β π β¦ π΄) β (πβπ§) = ((π¦ β π β¦ π΄)βπ§)) |
43 | | fveq2 6846 |
. . . 4
β’ (π§ = π΅ β ((π¦ β π β¦ π΄)βπ§) = ((π¦ β π β¦ π΄)βπ΅)) |
44 | 42, 43 | sylan9eq 2793 |
. . 3
β’ ((π = (π¦ β π β¦ π΄) β§ π§ = π΅) β (πβπ§) = ((π¦ β π β¦ π΄)βπ΅)) |
45 | 3, 21, 5, 20, 4, 41, 44 | cnmpt12 23041 |
. 2
β’ (π β (π₯ β π β¦ ((π¦ β π β¦ π΄)βπ΅)) β (π½ Cn πΏ)) |
46 | 31, 45 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) |