Step | Hyp | Ref
| Expression |
1 | | tgjustc1.p |
. . . . 5
β’ π = (BaseβπΊ) |
2 | 1 | fvexi 6904 |
. . . 4
β’ π β V |
3 | 2, 2 | xpex 7742 |
. . 3
β’ (π Γ π) β V |
4 | | tgjustf 27991 |
. . 3
β’ ((π Γ π) β V β βπ(π Er (π Γ π) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)))) |
5 | 3, 4 | ax-mp 5 |
. 2
β’
βπ(π Er (π Γ π) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) |
6 | | simplrl 773 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π€ β π) |
7 | | simplrr 774 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π₯ β π) |
8 | 6, 7 | opelxpd 5714 |
. . . . . 6
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β β¨π€, π₯β© β (π Γ π)) |
9 | | simprl 767 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π¦ β π) |
10 | | simprr 769 |
. . . . . . 7
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β π§ β π) |
11 | 9, 10 | opelxpd 5714 |
. . . . . 6
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β β¨π¦, π§β© β (π Γ π)) |
12 | | simpll 763 |
. . . . . 6
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) |
13 | | breq1 5150 |
. . . . . . . 8
β’ (π’ = β¨π€, π₯β© β (π’ππ£ β β¨π€, π₯β©ππ£)) |
14 | | fveq2 6890 |
. . . . . . . . . 10
β’ (π’ = β¨π€, π₯β© β ( β βπ’) = ( β ββ¨π€, π₯β©)) |
15 | | df-ov 7414 |
. . . . . . . . . 10
β’ (π€ β π₯) = ( β ββ¨π€, π₯β©) |
16 | 14, 15 | eqtr4di 2788 |
. . . . . . . . 9
β’ (π’ = β¨π€, π₯β© β ( β βπ’) = (π€ β π₯)) |
17 | 16 | eqeq1d 2732 |
. . . . . . . 8
β’ (π’ = β¨π€, π₯β© β (( β βπ’) = ( β βπ£) β (π€ β π₯) = ( β βπ£))) |
18 | 13, 17 | bibi12d 344 |
. . . . . . 7
β’ (π’ = β¨π€, π₯β© β ((π’ππ£ β ( β βπ’) = ( β βπ£)) β (β¨π€, π₯β©ππ£ β (π€ β π₯) = ( β βπ£)))) |
19 | | breq2 5151 |
. . . . . . . 8
β’ (π£ = β¨π¦, π§β© β (β¨π€, π₯β©ππ£ β β¨π€, π₯β©πβ¨π¦, π§β©)) |
20 | | fveq2 6890 |
. . . . . . . . . 10
β’ (π£ = β¨π¦, π§β© β ( β βπ£) = ( β ββ¨π¦, π§β©)) |
21 | | df-ov 7414 |
. . . . . . . . . 10
β’ (π¦ β π§) = ( β ββ¨π¦, π§β©) |
22 | 20, 21 | eqtr4di 2788 |
. . . . . . . . 9
β’ (π£ = β¨π¦, π§β© β ( β βπ£) = (π¦ β π§)) |
23 | 22 | eqeq2d 2741 |
. . . . . . . 8
β’ (π£ = β¨π¦, π§β© β ((π€ β π₯) = ( β βπ£) β (π€ β π₯) = (π¦ β π§))) |
24 | 19, 23 | bibi12d 344 |
. . . . . . 7
β’ (π£ = β¨π¦, π§β© β ((β¨π€, π₯β©ππ£ β (π€ β π₯) = ( β βπ£)) β (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§)))) |
25 | 18, 24 | rspc2va 3622 |
. . . . . 6
β’
(((β¨π€, π₯β© β (π Γ π) β§ β¨π¦, π§β© β (π Γ π)) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) β (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
26 | 8, 11, 12, 25 | syl21anc 834 |
. . . . 5
β’
(((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β§ (π¦ β π β§ π§ β π)) β (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
27 | 26 | ralrimivva 3198 |
. . . 4
β’
((βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β§ (π€ β π β§ π₯ β π)) β βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
28 | 27 | ralrimivva 3198 |
. . 3
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£)) β βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |
29 | 28 | anim2i 615 |
. 2
β’ ((π Er (π Γ π) β§ βπ’ β (π Γ π)βπ£ β (π Γ π)(π’ππ£ β ( β βπ’) = ( β βπ£))) β (π Er (π Γ π) β§ βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§)))) |
30 | 5, 29 | eximii 1837 |
1
β’
βπ(π Er (π Γ π) β§ βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) |