Step | Hyp | Ref
| Expression |
1 | | cnmptid.j |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
2 | | toponuni 22286 |
. . . 4
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
3 | | mpteq1 5202 |
. . . 4
β’ (π = βͺ
π½ β (π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) = (π₯ β βͺ π½ β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©)) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
β’ (π β (π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) = (π₯ β βͺ π½ β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©)) |
5 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β π) β π₯ β π) |
6 | | cnmpt11.a |
. . . . . . . . . 10
β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) |
7 | | cntop2 22615 |
. . . . . . . . . 10
β’ ((π₯ β π β¦ π΄) β (π½ Cn πΎ) β πΎ β Top) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ β Top) |
9 | | toptopon2 22290 |
. . . . . . . . 9
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
10 | 8, 9 | sylib 217 |
. . . . . . . 8
β’ (π β πΎ β (TopOnββͺ πΎ)) |
11 | | cnf2 22623 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ (π₯ β π β¦ π΄) β (π½ Cn πΎ)) β (π₯ β π β¦ π΄):πβΆβͺ πΎ) |
12 | 1, 10, 6, 11 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΄):πβΆβͺ πΎ) |
13 | 12 | fvmptelcdm 7065 |
. . . . . 6
β’ ((π β§ π₯ β π) β π΄ β βͺ πΎ) |
14 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
15 | 14 | fvmpt2 6963 |
. . . . . 6
β’ ((π₯ β π β§ π΄ β βͺ πΎ) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
16 | 5, 13, 15 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
17 | | cnmpt1t.b |
. . . . . . . . . 10
β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΏ)) |
18 | | cntop2 22615 |
. . . . . . . . . 10
β’ ((π₯ β π β¦ π΅) β (π½ Cn πΏ) β πΏ β Top) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (π β πΏ β Top) |
20 | | toptopon2 22290 |
. . . . . . . . 9
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
21 | 19, 20 | sylib 217 |
. . . . . . . 8
β’ (π β πΏ β (TopOnββͺ πΏ)) |
22 | | cnf2 22623 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΏ β (TopOnββͺ πΏ)
β§ (π₯ β π β¦ π΅) β (π½ Cn πΏ)) β (π₯ β π β¦ π΅):πβΆβͺ πΏ) |
23 | 1, 21, 17, 22 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΅):πβΆβͺ πΏ) |
24 | 23 | fvmptelcdm 7065 |
. . . . . 6
β’ ((π β§ π₯ β π) β π΅ β βͺ πΏ) |
25 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
26 | 25 | fvmpt2 6963 |
. . . . . 6
β’ ((π₯ β π β§ π΅ β βͺ πΏ) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
27 | 5, 24, 26 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
28 | 16, 27 | opeq12d 4842 |
. . . 4
β’ ((π β§ π₯ β π) β β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© = β¨π΄, π΅β©) |
29 | 28 | mpteq2dva 5209 |
. . 3
β’ (π β (π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) = (π₯ β π β¦ β¨π΄, π΅β©)) |
30 | 4, 29 | eqtr3d 2775 |
. 2
β’ (π β (π₯ β βͺ π½ β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) = (π₯ β π β¦ β¨π΄, π΅β©)) |
31 | | eqid 2733 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
32 | | nfcv 2904 |
. . . . 5
β’
β²π¦β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© |
33 | | nffvmpt1 6857 |
. . . . . 6
β’
β²π₯((π₯ β π β¦ π΄)βπ¦) |
34 | | nffvmpt1 6857 |
. . . . . 6
β’
β²π₯((π₯ β π β¦ π΅)βπ¦) |
35 | 33, 34 | nfop 4850 |
. . . . 5
β’
β²π₯β¨((π₯ β π β¦ π΄)βπ¦), ((π₯ β π β¦ π΅)βπ¦)β© |
36 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π¦ β ((π₯ β π β¦ π΄)βπ₯) = ((π₯ β π β¦ π΄)βπ¦)) |
37 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π¦ β ((π₯ β π β¦ π΅)βπ₯) = ((π₯ β π β¦ π΅)βπ¦)) |
38 | 36, 37 | opeq12d 4842 |
. . . . 5
β’ (π₯ = π¦ β β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© = β¨((π₯ β π β¦ π΄)βπ¦), ((π₯ β π β¦ π΅)βπ¦)β©) |
39 | 32, 35, 38 | cbvmpt 5220 |
. . . 4
β’ (π₯ β βͺ π½
β¦ β¨((π₯ β
π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) = (π¦ β βͺ π½ β¦ β¨((π₯ β π β¦ π΄)βπ¦), ((π₯ β π β¦ π΅)βπ¦)β©) |
40 | 31, 39 | txcnmpt 22998 |
. . 3
β’ (((π₯ β π β¦ π΄) β (π½ Cn πΎ) β§ (π₯ β π β¦ π΅) β (π½ Cn πΏ)) β (π₯ β βͺ π½ β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) β (π½ Cn (πΎ Γt πΏ))) |
41 | 6, 17, 40 | syl2anc 585 |
. 2
β’ (π β (π₯ β βͺ π½ β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) β (π½ Cn (πΎ Γt πΏ))) |
42 | 30, 41 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ β¨π΄, π΅β©) β (π½ Cn (πΎ Γt πΏ))) |