Step | Hyp | Ref
| Expression |
1 | | cnmpt21.j |
. 2
β’ (π β π½ β (TopOnβπ)) |
2 | | cnmpt21.k |
. 2
β’ (π β πΎ β (TopOnβπ)) |
3 | | cnmpt21.a |
. 2
β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) |
4 | | cnmpt2t.b |
. 2
β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΎ) Cn π)) |
5 | | cntop2 22608 |
. . . 4
β’ ((π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ) β πΏ β Top) |
6 | 3, 5 | syl 17 |
. . 3
β’ (π β πΏ β Top) |
7 | | toptopon2 22283 |
. . 3
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
8 | 6, 7 | sylib 217 |
. 2
β’ (π β πΏ β (TopOnββͺ πΏ)) |
9 | | cntop2 22608 |
. . . 4
β’ ((π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΎ) Cn π) β π β Top) |
10 | 4, 9 | syl 17 |
. . 3
β’ (π β π β Top) |
11 | | toptopon2 22283 |
. . 3
β’ (π β Top β π β (TopOnββͺ π)) |
12 | 10, 11 | sylib 217 |
. 2
β’ (π β π β (TopOnββͺ π)) |
13 | | txtopon 22958 |
. . . . . . 7
β’ ((πΏ β (TopOnββͺ πΏ)
β§ π β
(TopOnββͺ π)) β (πΏ Γt π) β (TopOnβ(βͺ πΏ
Γ βͺ π))) |
14 | 8, 12, 13 | syl2anc 585 |
. . . . . 6
β’ (π β (πΏ Γt π) β (TopOnβ(βͺ πΏ
Γ βͺ π))) |
15 | | cnmpt22f.f |
. . . . . . . 8
β’ (π β πΉ β ((πΏ Γt π) Cn π)) |
16 | | cntop2 22608 |
. . . . . . . 8
β’ (πΉ β ((πΏ Γt π) Cn π) β π β Top) |
17 | 15, 16 | syl 17 |
. . . . . . 7
β’ (π β π β Top) |
18 | | toptopon2 22283 |
. . . . . . 7
β’ (π β Top β π β (TopOnββͺ π)) |
19 | 17, 18 | sylib 217 |
. . . . . 6
β’ (π β π β (TopOnββͺ π)) |
20 | | cnf2 22616 |
. . . . . 6
β’ (((πΏ Γt π) β (TopOnβ(βͺ πΏ
Γ βͺ π)) β§ π β (TopOnββͺ π)
β§ πΉ β ((πΏ Γt π) Cn π)) β πΉ:(βͺ πΏ Γ βͺ π)βΆβͺ π) |
21 | 14, 19, 15, 20 | syl3anc 1372 |
. . . . 5
β’ (π β πΉ:(βͺ πΏ Γ βͺ π)βΆβͺ π) |
22 | 21 | ffnd 6670 |
. . . 4
β’ (π β πΉ Fn (βͺ πΏ Γ βͺ π)) |
23 | | fnov 7488 |
. . . 4
β’ (πΉ Fn (βͺ πΏ
Γ βͺ π) β πΉ = (π§ β βͺ πΏ, π€ β βͺ π β¦ (π§πΉπ€))) |
24 | 22, 23 | sylib 217 |
. . 3
β’ (π β πΉ = (π§ β βͺ πΏ, π€ β βͺ π β¦ (π§πΉπ€))) |
25 | 24, 15 | eqeltrrd 2835 |
. 2
β’ (π β (π§ β βͺ πΏ, π€ β βͺ π β¦ (π§πΉπ€)) β ((πΏ Γt π) Cn π)) |
26 | | oveq12 7367 |
. 2
β’ ((π§ = π΄ β§ π€ = π΅) β (π§πΉπ€) = (π΄πΉπ΅)) |
27 | 1, 2, 3, 4, 8, 12,
25, 26 | cnmpt22 23041 |
1
β’ (π β (π₯ β π, π¦ β π β¦ (π΄πΉπ΅)) β ((π½ Γt πΎ) Cn π)) |