Step | Hyp | Ref
| Expression |
1 | | tgjustc1.p |
. . . . 5
β’ π = (BaseβπΊ) |
2 | 1 | fvexi 6860 |
. . . 4
β’ π β V |
3 | 2, 2 | xpex 7691 |
. . 3
β’ (π Γ π) β V |
4 | | tgjustf 27464 |
. . 3
β’ ((π Γ π) β V β βπ(π Er (π Γ π) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)))) |
5 | 3, 4 | ax-mp 5 |
. 2
β’
βπ(π Er (π Γ π) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) |
6 | | simplrl 776 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π€ β π) |
7 | | simplrr 777 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π₯ β π) |
8 | 6, 7 | opelxpd 5675 |
. . . . . 6
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β β¨π€, π₯β© β (π Γ π)) |
9 | | simprl 770 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π¦ β π) |
10 | | simprr 772 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π§ β π) |
11 | 9, 10 | opelxpd 5675 |
. . . . . 6
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β β¨π¦, π§β© β (π Γ π)) |
12 | | simpll 766 |
. . . . . 6
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) |
13 | | breq1 5112 |
. . . . . . . 8
β’ (π’ = β¨π€, π₯β© β (π’ππ£ β β¨π€, π₯β©ππ£)) |
14 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π’ = β¨π€, π₯β© β ( β βπ’) = ( β ββ¨π€, π₯β©)) |
15 | | df-ov 7364 |
. . . . . . . . . 10
β’ (π€ β π₯) = ( β ββ¨π€, π₯β©) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π’ = β¨π€, π₯β© β ( β βπ’) = (π€ β π₯)) |
17 | 16 | eqeq1d 2735 |
. . . . . . . 8
β’ (π’ = β¨π€, π₯β© β (( β βπ’) = ( β βπ£) β (π€ β π₯) = ( β βπ£))) |
18 | 13, 17 | bibi12d 346 |
. . . . . . 7
β’ (π’ = β¨π€, π₯β© β ((π’ππ£ β ( β βπ’) = ( β βπ£)) β (β¨π€, π₯β©ππ£ β (π€ β π₯) = ( β βπ£)))) |
19 | | breq2 5113 |
. . . . . . . 8
β’ (π£ = β¨π¦, π§β© β (β¨π€, π₯β©ππ£ β β¨π€, π₯β©πβ¨π¦, π§β©)) |
20 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π£ = β¨π¦, π§β© β ( β βπ£) = ( β ββ¨π¦, π§β©)) |
21 | | df-ov 7364 |
. . . . . . . . . 10
β’ (π¦ β π§) = ( β ββ¨π¦, π§β©) |
22 | 20, 21 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π£ = β¨π¦, π§β© β ( β βπ£) = (π¦ β π§)) |
23 | 22 | eqeq2d 2744 |
. . . . . . . 8
β’ (π£ = β¨π¦, π§β© β ((π€ β π₯) = ( β βπ£) β (π€ β π₯) = (π¦ β π§))) |
24 | 19, 23 | bibi12d 346 |
. . . . . . 7
β’ (π£ = β¨π¦, π§β© β ((β¨π€, π₯β©ππ£ β (π€ β π₯) = ( β βπ£)) β (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§)))) |
25 | 18, 24 | rspc2va 3593 |
. . . . . 6
β’
(((β¨π€, π₯β© β (π Γ π) β§ β¨π¦, π§β© β (π Γ π)) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) β (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
26 | 8, 11, 12, 25 | syl21anc 837 |
. . . . 5
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
27 | 26 | ralrimivva 3194 |
. . . 4
β’
((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
28 | 27 | ralrimivva 3194 |
. . 3
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
29 | 28 | anim2i 618 |
. 2
β’ ((π Er (π Γ π) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) β (π Er (π Γ π) β§ βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§)))) |
30 | 5, 29 | eximii 1840 |
1
β’
βπ(π Er (π Γ π) β§ βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |