Step | Hyp | Ref
| Expression |
1 | | df-ov 7364 |
. . . . . . . . . 10
β’ (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = ((π₯ β π, π¦ β π β¦ π΄)ββ¨π₯, π¦β©) |
2 | | simprl 770 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
3 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
4 | | cnmpt21.j |
. . . . . . . . . . . . . . . 16
β’ (π β π½ β (TopOnβπ)) |
5 | | cnmpt21.k |
. . . . . . . . . . . . . . . 16
β’ (π β πΎ β (TopOnβπ)) |
6 | | txtopon 22965 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
7 | 4, 5, 6 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
8 | | cnmpt21.l |
. . . . . . . . . . . . . . 15
β’ (π β πΏ β (TopOnβπ)) |
9 | | cnmpt21.a |
. . . . . . . . . . . . . . 15
β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) |
10 | | cnf2 22623 |
. . . . . . . . . . . . . . 15
β’ (((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§ πΏ β (TopOnβπ) β§ (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆπ) |
11 | 7, 8, 9, 10 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆπ) |
12 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π, π¦ β π β¦ π΄) = (π₯ β π, π¦ β π β¦ π΄) |
13 | 12 | fmpo 8004 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
π βπ¦ β π π΄ β π β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆπ) |
14 | 11, 13 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π β βπ₯ β π βπ¦ β π π΄ β π) |
15 | | rsp2 3259 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π βπ¦ β π π΄ β π β ((π₯ β π β§ π¦ β π) β π΄ β π)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((π₯ β π β§ π¦ β π) β π΄ β π)) |
17 | 16 | imp 408 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π΄ β π) |
18 | 12 | ovmpt4g 7506 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π β§ π΄ β π) β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = π΄) |
19 | 2, 3, 17, 18 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = π΄) |
20 | 1, 19 | eqtr3id 2787 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯ β π, π¦ β π β¦ π΄)ββ¨π₯, π¦β©) = π΄) |
21 | 20 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π§ β π β¦ π΅)β((π₯ β π, π¦ β π β¦ π΄)ββ¨π₯, π¦β©)) = ((π§ β π β¦ π΅)βπ΄)) |
22 | | eqid 2733 |
. . . . . . . . 9
β’ (π§ β π β¦ π΅) = (π§ β π β¦ π΅) |
23 | | cnmpt21.c |
. . . . . . . . 9
β’ (π§ = π΄ β π΅ = πΆ) |
24 | 23 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π§ = π΄ β (π΅ β βͺ π β πΆ β βͺ π)) |
25 | | cnmpt21.b |
. . . . . . . . . . . . . . 15
β’ (π β (π§ β π β¦ π΅) β (πΏ Cn π)) |
26 | | cntop2 22615 |
. . . . . . . . . . . . . . 15
β’ ((π§ β π β¦ π΅) β (πΏ Cn π) β π β Top) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β Top) |
28 | | toptopon2 22290 |
. . . . . . . . . . . . . 14
β’ (π β Top β π β (TopOnββͺ π)) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β π β (TopOnββͺ π)) |
30 | | cnf2 22623 |
. . . . . . . . . . . . 13
β’ ((πΏ β (TopOnβπ) β§ π β (TopOnββͺ π)
β§ (π§ β π β¦ π΅) β (πΏ Cn π)) β (π§ β π β¦ π΅):πβΆβͺ π) |
31 | 8, 29, 25, 30 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β (π§ β π β¦ π΅):πβΆβͺ π) |
32 | 22 | fmpt 7062 |
. . . . . . . . . . . 12
β’
(βπ§ β
π π΅ β βͺ π β (π§ β π β¦ π΅):πβΆβͺ π) |
33 | 31, 32 | sylibr 233 |
. . . . . . . . . . 11
β’ (π β βπ§ β π π΅ β βͺ π) |
34 | 33 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π)) β βπ§ β π π΅ β βͺ π) |
35 | 24, 34, 17 | rspcdva 3584 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π)) β πΆ β βͺ π) |
36 | 22, 23, 17, 35 | fvmptd3 6975 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π§ β π β¦ π΅)βπ΄) = πΆ) |
37 | 21, 36 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π§ β π β¦ π΅)β((π₯ β π, π¦ β π β¦ π΄)ββ¨π₯, π¦β©)) = πΆ) |
38 | | opelxpi 5674 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β π) β β¨π₯, π¦β© β (π Γ π)) |
39 | | fvco3 6944 |
. . . . . . . 8
β’ (((π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆπ β§ β¨π₯, π¦β© β (π Γ π)) β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π§ β π β¦ π΅)β((π₯ β π, π¦ β π β¦ π΄)ββ¨π₯, π¦β©))) |
40 | 11, 38, 39 | syl2an 597 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π§ β π β¦ π΅)β((π₯ β π, π¦ β π β¦ π΄)ββ¨π₯, π¦β©))) |
41 | | df-ov 7364 |
. . . . . . . 8
β’ (π₯(π₯ β π, π¦ β π β¦ πΆ)π¦) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) |
42 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π, π¦ β π β¦ πΆ) = (π₯ β π, π¦ β π β¦ πΆ) |
43 | 42 | ovmpt4g 7506 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π β§ πΆ β βͺ π) β (π₯(π₯ β π, π¦ β π β¦ πΆ)π¦) = πΆ) |
44 | 2, 3, 35, 43 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(π₯ β π, π¦ β π β¦ πΆ)π¦) = πΆ) |
45 | 41, 44 | eqtr3id 2787 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) = πΆ) |
46 | 37, 40, 45 | 3eqtr4d 2783 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©)) |
47 | 46 | ralrimivva 3194 |
. . . . 5
β’ (π β βπ₯ β π βπ¦ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©)) |
48 | | nfv 1918 |
. . . . . 6
β’
β²π’βπ¦ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) |
49 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯π |
50 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π₯(π§ β π β¦ π΅) |
51 | | nfmpo1 7441 |
. . . . . . . . . 10
β’
β²π₯(π₯ β π, π¦ β π β¦ π΄) |
52 | 50, 51 | nfco 5825 |
. . . . . . . . 9
β’
β²π₯((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) |
53 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π₯β¨π’, π£β© |
54 | 52, 53 | nffv 6856 |
. . . . . . . 8
β’
β²π₯(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) |
55 | | nfmpo1 7441 |
. . . . . . . . 9
β’
β²π₯(π₯ β π, π¦ β π β¦ πΆ) |
56 | 55, 53 | nffv 6856 |
. . . . . . . 8
β’
β²π₯((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©) |
57 | 54, 56 | nfeq 2917 |
. . . . . . 7
β’
β²π₯(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©) |
58 | 49, 57 | nfralw 3293 |
. . . . . 6
β’
β²π₯βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©) |
59 | | nfv 1918 |
. . . . . . . 8
β’
β²π£(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) |
60 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π¦(π§ β π β¦ π΅) |
61 | | nfmpo2 7442 |
. . . . . . . . . . 11
β’
β²π¦(π₯ β π, π¦ β π β¦ π΄) |
62 | 60, 61 | nfco 5825 |
. . . . . . . . . 10
β’
β²π¦((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) |
63 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π¦β¨π₯, π£β© |
64 | 62, 63 | nffv 6856 |
. . . . . . . . 9
β’
β²π¦(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©) |
65 | | nfmpo2 7442 |
. . . . . . . . . 10
β’
β²π¦(π₯ β π, π¦ β π β¦ πΆ) |
66 | 65, 63 | nffv 6856 |
. . . . . . . . 9
β’
β²π¦((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©) |
67 | 64, 66 | nfeq 2917 |
. . . . . . . 8
β’
β²π¦(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©) |
68 | | opeq2 4835 |
. . . . . . . . . 10
β’ (π¦ = π£ β β¨π₯, π¦β© = β¨π₯, π£β©) |
69 | 68 | fveq2d 6850 |
. . . . . . . . 9
β’ (π¦ = π£ β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©)) |
70 | 68 | fveq2d 6850 |
. . . . . . . . 9
β’ (π¦ = π£ β ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©)) |
71 | 69, 70 | eqeq12d 2749 |
. . . . . . . 8
β’ (π¦ = π£ β ((((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©))) |
72 | 59, 67, 71 | cbvralw 3288 |
. . . . . . 7
β’
(βπ¦ β
π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) β βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©)) |
73 | | opeq1 4834 |
. . . . . . . . . 10
β’ (π₯ = π’ β β¨π₯, π£β© = β¨π’, π£β©) |
74 | 73 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = π’ β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©) = (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©)) |
75 | 73 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = π’ β ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©)) |
76 | 74, 75 | eqeq12d 2749 |
. . . . . . . 8
β’ (π₯ = π’ β ((((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©) β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©))) |
77 | 76 | ralbidv 3171 |
. . . . . . 7
β’ (π₯ = π’ β (βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π£β©) β βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©))) |
78 | 72, 77 | bitrid 283 |
. . . . . 6
β’ (π₯ = π’ β (βπ¦ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) β βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©))) |
79 | 48, 58, 78 | cbvralw 3288 |
. . . . 5
β’
(βπ₯ β
π βπ¦ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π₯, π¦β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π₯, π¦β©) β βπ’ β π βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©)) |
80 | 47, 79 | sylib 217 |
. . . 4
β’ (π β βπ’ β π βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©)) |
81 | | fveq2 6846 |
. . . . . 6
β’ (π€ = β¨π’, π£β© β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))βπ€) = (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©)) |
82 | | fveq2 6846 |
. . . . . 6
β’ (π€ = β¨π’, π£β© β ((π₯ β π, π¦ β π β¦ πΆ)βπ€) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©)) |
83 | 81, 82 | eqeq12d 2749 |
. . . . 5
β’ (π€ = β¨π’, π£β© β ((((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))βπ€) = ((π₯ β π, π¦ β π β¦ πΆ)βπ€) β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©))) |
84 | 83 | ralxp 5801 |
. . . 4
β’
(βπ€ β
(π Γ π)(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))βπ€) = ((π₯ β π, π¦ β π β¦ πΆ)βπ€) β βπ’ β π βπ£ β π (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))ββ¨π’, π£β©) = ((π₯ β π, π¦ β π β¦ πΆ)ββ¨π’, π£β©)) |
85 | 80, 84 | sylibr 233 |
. . 3
β’ (π β βπ€ β (π Γ π)(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))βπ€) = ((π₯ β π, π¦ β π β¦ πΆ)βπ€)) |
86 | | fco 6696 |
. . . . . 6
β’ (((π§ β π β¦ π΅):πβΆβͺ π β§ (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆπ) β ((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)):(π Γ π)βΆβͺ π) |
87 | 31, 11, 86 | syl2anc 585 |
. . . . 5
β’ (π β ((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)):(π Γ π)βΆβͺ π) |
88 | 87 | ffnd 6673 |
. . . 4
β’ (π β ((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) Fn (π Γ π)) |
89 | 35 | ralrimivva 3194 |
. . . . . 6
β’ (π β βπ₯ β π βπ¦ β π πΆ β βͺ π) |
90 | 42 | fmpo 8004 |
. . . . . 6
β’
(βπ₯ β
π βπ¦ β π πΆ β βͺ π β (π₯ β π, π¦ β π β¦ πΆ):(π Γ π)βΆβͺ π) |
91 | 89, 90 | sylib 217 |
. . . . 5
β’ (π β (π₯ β π, π¦ β π β¦ πΆ):(π Γ π)βΆβͺ π) |
92 | 91 | ffnd 6673 |
. . . 4
β’ (π β (π₯ β π, π¦ β π β¦ πΆ) Fn (π Γ π)) |
93 | | eqfnfv 6986 |
. . . 4
β’ ((((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) Fn (π Γ π) β§ (π₯ β π, π¦ β π β¦ πΆ) Fn (π Γ π)) β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) = (π₯ β π, π¦ β π β¦ πΆ) β βπ€ β (π Γ π)(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))βπ€) = ((π₯ β π, π¦ β π β¦ πΆ)βπ€))) |
94 | 88, 92, 93 | syl2anc 585 |
. . 3
β’ (π β (((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) = (π₯ β π, π¦ β π β¦ πΆ) β βπ€ β (π Γ π)(((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄))βπ€) = ((π₯ β π, π¦ β π β¦ πΆ)βπ€))) |
95 | 85, 94 | mpbird 257 |
. 2
β’ (π β ((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) = (π₯ β π, π¦ β π β¦ πΆ)) |
96 | | cnco 22640 |
. . 3
β’ (((π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ) β§ (π§ β π β¦ π΅) β (πΏ Cn π)) β ((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) β ((π½ Γt πΎ) Cn π)) |
97 | 9, 25, 96 | syl2anc 585 |
. 2
β’ (π β ((π§ β π β¦ π΅) β (π₯ β π, π¦ β π β¦ π΄)) β ((π½ Γt πΎ) Cn π)) |
98 | 95, 97 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π, π¦ β π β¦ πΆ) β ((π½ Γt πΎ) Cn π)) |