Step | Hyp | Ref
| Expression |
1 | | cnmpt1plusg.k |
. . . . . . . . . 10
β’ (π β πΎ β (TopOnβπ)) |
2 | | cnmpt2plusg.l |
. . . . . . . . . 10
β’ (π β πΏ β (TopOnβπ)) |
3 | | txtopon 22894 |
. . . . . . . . . 10
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnβπ)) β (πΎ Γt πΏ) β (TopOnβ(π Γ π))) |
4 | 1, 2, 3 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (πΎ Γt πΏ) β (TopOnβ(π Γ π))) |
5 | | cnmpt1plusg.g |
. . . . . . . . . 10
β’ (π β πΊ β TopMnd) |
6 | | tgpcn.j |
. . . . . . . . . . 11
β’ π½ = (TopOpenβπΊ) |
7 | | eqid 2737 |
. . . . . . . . . . 11
β’
(BaseβπΊ) =
(BaseβπΊ) |
8 | 6, 7 | tmdtopon 23384 |
. . . . . . . . . 10
β’ (πΊ β TopMnd β π½ β
(TopOnβ(BaseβπΊ))) |
9 | 5, 8 | syl 17 |
. . . . . . . . 9
β’ (π β π½ β (TopOnβ(BaseβπΊ))) |
10 | | cnmpt2plusg.a |
. . . . . . . . 9
β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt πΏ) Cn π½)) |
11 | | cnf2 22552 |
. . . . . . . . 9
β’ (((πΎ Γt πΏ) β (TopOnβ(π Γ π)) β§ π½ β (TopOnβ(BaseβπΊ)) β§ (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt πΏ) Cn π½)) β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆ(BaseβπΊ)) |
12 | 4, 9, 10, 11 | syl3anc 1371 |
. . . . . . . 8
β’ (π β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆ(BaseβπΊ)) |
13 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β π, π¦ β π β¦ π΄) = (π₯ β π, π¦ β π β¦ π΄) |
14 | 13 | fmpo 7992 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π π΄ β (BaseβπΊ) β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆ(BaseβπΊ)) |
15 | 12, 14 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β π βπ¦ β π π΄ β (BaseβπΊ)) |
16 | 15 | r19.21bi 3232 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π π΄ β (BaseβπΊ)) |
17 | 16 | r19.21bi 3232 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β π΄ β (BaseβπΊ)) |
18 | 17 | 3impa 1110 |
. . . 4
β’ ((π β§ π₯ β π β§ π¦ β π) β π΄ β (BaseβπΊ)) |
19 | | cnmpt2plusg.b |
. . . . . . . . 9
β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΎ Γt πΏ) Cn π½)) |
20 | | cnf2 22552 |
. . . . . . . . 9
β’ (((πΎ Γt πΏ) β (TopOnβ(π Γ π)) β§ π½ β (TopOnβ(BaseβπΊ)) β§ (π₯ β π, π¦ β π β¦ π΅) β ((πΎ Γt πΏ) Cn π½)) β (π₯ β π, π¦ β π β¦ π΅):(π Γ π)βΆ(BaseβπΊ)) |
21 | 4, 9, 19, 20 | syl3anc 1371 |
. . . . . . . 8
β’ (π β (π₯ β π, π¦ β π β¦ π΅):(π Γ π)βΆ(BaseβπΊ)) |
22 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β π, π¦ β π β¦ π΅) = (π₯ β π, π¦ β π β¦ π΅) |
23 | 22 | fmpo 7992 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π π΅ β (BaseβπΊ) β (π₯ β π, π¦ β π β¦ π΅):(π Γ π)βΆ(BaseβπΊ)) |
24 | 21, 23 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β π βπ¦ β π π΅ β (BaseβπΊ)) |
25 | 24 | r19.21bi 3232 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π π΅ β (BaseβπΊ)) |
26 | 25 | r19.21bi 3232 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β π΅ β (BaseβπΊ)) |
27 | 26 | 3impa 1110 |
. . . 4
β’ ((π β§ π₯ β π β§ π¦ β π) β π΅ β (BaseβπΊ)) |
28 | | cnmpt1plusg.p |
. . . . 5
β’ + =
(+gβπΊ) |
29 | | eqid 2737 |
. . . . 5
β’
(+πβπΊ) = (+πβπΊ) |
30 | 7, 28, 29 | plusfval 18464 |
. . . 4
β’ ((π΄ β (BaseβπΊ) β§ π΅ β (BaseβπΊ)) β (π΄(+πβπΊ)π΅) = (π΄ + π΅)) |
31 | 18, 27, 30 | syl2anc 584 |
. . 3
β’ ((π β§ π₯ β π β§ π¦ β π) β (π΄(+πβπΊ)π΅) = (π΄ + π΅)) |
32 | 31 | mpoeq3dva 7428 |
. 2
β’ (π β (π₯ β π, π¦ β π β¦ (π΄(+πβπΊ)π΅)) = (π₯ β π, π¦ β π β¦ (π΄ + π΅))) |
33 | 6, 29 | tmdcn 23386 |
. . . 4
β’ (πΊ β TopMnd β
(+πβπΊ) β ((π½ Γt π½) Cn π½)) |
34 | 5, 33 | syl 17 |
. . 3
β’ (π β
(+πβπΊ) β ((π½ Γt π½) Cn π½)) |
35 | 1, 2, 10, 19, 34 | cnmpt22f 22978 |
. 2
β’ (π β (π₯ β π, π¦ β π β¦ (π΄(+πβπΊ)π΅)) β ((πΎ Γt πΏ) Cn π½)) |
36 | 32, 35 | eqeltrrd 2839 |
1
β’ (π β (π₯ β π, π¦ β π β¦ (π΄ + π΅)) β ((πΎ Γt πΏ) Cn π½)) |