Step | Hyp | Ref
| Expression |
1 | | cnmptid.j |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
2 | | cnmpt12.k |
. . . . . 6
β’ (π β πΎ β (TopOnβπ)) |
3 | | cnmpt11.a |
. . . . . 6
β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) |
4 | | cnf2 22623 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ (π₯ β π β¦ π΄) β (π½ Cn πΎ)) β (π₯ β π β¦ π΄):πβΆπ) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. . . . 5
β’ (π β (π₯ β π β¦ π΄):πβΆπ) |
6 | 5 | fvmptelcdm 7065 |
. . . 4
β’ ((π β§ π₯ β π) β π΄ β π) |
7 | | cnmpt12.l |
. . . . . 6
β’ (π β πΏ β (TopOnβπ)) |
8 | | cnmpt1t.b |
. . . . . 6
β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΏ)) |
9 | | cnf2 22623 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΏ β (TopOnβπ) β§ (π₯ β π β¦ π΅) β (π½ Cn πΏ)) β (π₯ β π β¦ π΅):πβΆπ) |
10 | 1, 7, 8, 9 | syl3anc 1372 |
. . . . 5
β’ (π β (π₯ β π β¦ π΅):πβΆπ) |
11 | 10 | fvmptelcdm 7065 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β π) |
12 | 6, 11 | jca 513 |
. . . . 5
β’ ((π β§ π₯ β π) β (π΄ β π β§ π΅ β π)) |
13 | | txtopon 22965 |
. . . . . . . . . 10
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnβπ)) β (πΎ Γt πΏ) β (TopOnβ(π Γ π))) |
14 | 2, 7, 13 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΎ Γt πΏ) β (TopOnβ(π Γ π))) |
15 | | cnmpt12.c |
. . . . . . . . . . 11
β’ (π β (π¦ β π, π§ β π β¦ πΆ) β ((πΎ Γt πΏ) Cn π)) |
16 | | cntop2 22615 |
. . . . . . . . . . 11
β’ ((π¦ β π, π§ β π β¦ πΆ) β ((πΎ Γt πΏ) Cn π) β π β Top) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
β’ (π β π β Top) |
18 | | toptopon2 22290 |
. . . . . . . . . 10
β’ (π β Top β π β (TopOnββͺ π)) |
19 | 17, 18 | sylib 217 |
. . . . . . . . 9
β’ (π β π β (TopOnββͺ π)) |
20 | | cnf2 22623 |
. . . . . . . . 9
β’ (((πΎ Γt πΏ) β (TopOnβ(π Γ π)) β§ π β (TopOnββͺ π)
β§ (π¦ β π, π§ β π β¦ πΆ) β ((πΎ Γt πΏ) Cn π)) β (π¦ β π, π§ β π β¦ πΆ):(π Γ π)βΆβͺ π) |
21 | 14, 19, 15, 20 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π¦ β π, π§ β π β¦ πΆ):(π Γ π)βΆβͺ π) |
22 | | eqid 2733 |
. . . . . . . . 9
β’ (π¦ β π, π§ β π β¦ πΆ) = (π¦ β π, π§ β π β¦ πΆ) |
23 | 22 | fmpo 8004 |
. . . . . . . 8
β’
(βπ¦ β
π βπ§ β π πΆ β βͺ π β (π¦ β π, π§ β π β¦ πΆ):(π Γ π)βΆβͺ π) |
24 | 21, 23 | sylibr 233 |
. . . . . . 7
β’ (π β βπ¦ β π βπ§ β π πΆ β βͺ π) |
25 | | r2al 3188 |
. . . . . . 7
β’
(βπ¦ β
π βπ§ β π πΆ β βͺ π β βπ¦βπ§((π¦ β π β§ π§ β π) β πΆ β βͺ π)) |
26 | 24, 25 | sylib 217 |
. . . . . 6
β’ (π β βπ¦βπ§((π¦ β π β§ π§ β π) β πΆ β βͺ π)) |
27 | 26 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β βπ¦βπ§((π¦ β π β§ π§ β π) β πΆ β βͺ π)) |
28 | | eleq1 2822 |
. . . . . . . 8
β’ (π¦ = π΄ β (π¦ β π β π΄ β π)) |
29 | | eleq1 2822 |
. . . . . . . 8
β’ (π§ = π΅ β (π§ β π β π΅ β π)) |
30 | 28, 29 | bi2anan9 638 |
. . . . . . 7
β’ ((π¦ = π΄ β§ π§ = π΅) β ((π¦ β π β§ π§ β π) β (π΄ β π β§ π΅ β π))) |
31 | | cnmpt12.d |
. . . . . . . 8
β’ ((π¦ = π΄ β§ π§ = π΅) β πΆ = π·) |
32 | 31 | eleq1d 2819 |
. . . . . . 7
β’ ((π¦ = π΄ β§ π§ = π΅) β (πΆ β βͺ π β π· β βͺ π)) |
33 | 30, 32 | imbi12d 345 |
. . . . . 6
β’ ((π¦ = π΄ β§ π§ = π΅) β (((π¦ β π β§ π§ β π) β πΆ β βͺ π) β ((π΄ β π β§ π΅ β π) β π· β βͺ π))) |
34 | 33 | spc2gv 3561 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β (βπ¦βπ§((π¦ β π β§ π§ β π) β πΆ β βͺ π) β ((π΄ β π β§ π΅ β π) β π· β βͺ π))) |
35 | 12, 27, 12, 34 | syl3c 66 |
. . . 4
β’ ((π β§ π₯ β π) β π· β βͺ π) |
36 | 31, 22 | ovmpoga 7513 |
. . . 4
β’ ((π΄ β π β§ π΅ β π β§ π· β βͺ π) β (π΄(π¦ β π, π§ β π β¦ πΆ)π΅) = π·) |
37 | 6, 11, 35, 36 | syl3anc 1372 |
. . 3
β’ ((π β§ π₯ β π) β (π΄(π¦ β π, π§ β π β¦ πΆ)π΅) = π·) |
38 | 37 | mpteq2dva 5209 |
. 2
β’ (π β (π₯ β π β¦ (π΄(π¦ β π, π§ β π β¦ πΆ)π΅)) = (π₯ β π β¦ π·)) |
39 | 1, 3, 8, 15 | cnmpt12f 23040 |
. 2
β’ (π β (π₯ β π β¦ (π΄(π¦ β π, π§ β π β¦ πΆ)π΅)) β (π½ Cn π)) |
40 | 38, 39 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ π·) β (π½ Cn π)) |