Step | Hyp | Ref
| Expression |
1 | | simp-4r 781 |
. . . . 5
β’
((((((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β§ π₯ β π) β§ π¦ β π) β§ π = β¨π₯, π¦β©) β ( β βπ) = π΄) |
2 | | simpr 485 |
. . . . . 6
β’
((((((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β§ π₯ β π) β§ π¦ β π) β§ π = β¨π₯, π¦β©) β π = β¨π₯, π¦β©) |
3 | 2 | fveq2d 6829 |
. . . . 5
β’
((((((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β§ π₯ β π) β§ π¦ β π) β§ π = β¨π₯, π¦β©) β ( β βπ) = ( β ββ¨π₯, π¦β©)) |
4 | 1, 3 | eqtr3d 2778 |
. . . 4
β’
((((((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β§ π₯ β π) β§ π¦ β π) β§ π = β¨π₯, π¦β©) β π΄ = ( β ββ¨π₯, π¦β©)) |
5 | | df-ov 7340 |
. . . 4
β’ (π₯ β π¦) = ( β ββ¨π₯, π¦β©) |
6 | 4, 5 | eqtr4di 2794 |
. . 3
β’
((((((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β§ π₯ β π) β§ π¦ β π) β§ π = β¨π₯, π¦β©) β π΄ = (π₯ β π¦)) |
7 | | simplr 766 |
. . . 4
β’ (((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β π β (π Γ π)) |
8 | | elxp2 5644 |
. . . 4
β’ (π β (π Γ π) β βπ₯ β π βπ¦ β π π = β¨π₯, π¦β©) |
9 | 7, 8 | sylib 217 |
. . 3
β’ (((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β βπ₯ β π βπ¦ β π π = β¨π₯, π¦β©) |
10 | 6, 9 | reximddv2 3202 |
. 2
β’ (((π β§ π β (π Γ π)) β§ ( β βπ) = π΄) β βπ₯ β π βπ¦ β π π΄ = (π₯ β π¦)) |
11 | | legso.f |
. . 3
β’ (π β Fun β ) |
12 | | ltgseg.p |
. . . 4
β’ (π β π΄ β πΈ) |
13 | | legso.a |
. . . 4
β’ πΈ = ( β β (π Γ π)) |
14 | 12, 13 | eleqtrdi 2847 |
. . 3
β’ (π β π΄ β ( β β (π Γ π))) |
15 | | fvelima 6891 |
. . 3
β’ ((Fun
β
β§ π΄ β ( β β
(π Γ π))) β βπ β (π Γ π)( β βπ) = π΄) |
16 | 11, 14, 15 | syl2anc 584 |
. 2
β’ (π β βπ β (π Γ π)( β βπ) = π΄) |
17 | 10, 16 | r19.29a 3155 |
1
β’ (π β βπ₯ β π βπ¦ β π π΄ = (π₯ β π¦)) |