Step | Hyp | Ref
| Expression |
1 | | opex 5422 |
. 2
β’
β¨π΄, π΅β© β V |
2 | | brcart.3 |
. 2
β’ πΆ β V |
3 | | df-cart 34496 |
. 2
β’ Cart =
(((V Γ V) Γ V) β ran ((V β E ) β³ (pprod( E , E
) β V))) |
4 | | brcart.1 |
. . . 4
β’ π΄ β V |
5 | | brcart.2 |
. . . 4
β’ π΅ β V |
6 | 4, 5 | opelvv 5673 |
. . 3
β’
β¨π΄, π΅β© β (V Γ
V) |
7 | | brxp 5682 |
. . 3
β’
(β¨π΄, π΅β©((V Γ V) Γ
V)πΆ β (β¨π΄, π΅β© β (V Γ V) β§ πΆ β V)) |
8 | 6, 2, 7 | mpbir2an 710 |
. 2
β’
β¨π΄, π΅β©((V Γ V) Γ
V)πΆ |
9 | | 3anass 1096 |
. . . . 5
β’ ((π₯ = β¨π¦, π§β© β§ π¦ E π΄ β§ π§ E π΅) β (π₯ = β¨π¦, π§β© β§ (π¦ E π΄ β§ π§ E π΅))) |
10 | 4 | epeli 5540 |
. . . . . . 7
β’ (π¦ E π΄ β π¦ β π΄) |
11 | 5 | epeli 5540 |
. . . . . . 7
β’ (π§ E π΅ β π§ β π΅) |
12 | 10, 11 | anbi12i 628 |
. . . . . 6
β’ ((π¦ E π΄ β§ π§ E π΅) β (π¦ β π΄ β§ π§ β π΅)) |
13 | 12 | anbi2i 624 |
. . . . 5
β’ ((π₯ = β¨π¦, π§β© β§ (π¦ E π΄ β§ π§ E π΅)) β (π₯ = β¨π¦, π§β© β§ (π¦ β π΄ β§ π§ β π΅))) |
14 | 9, 13 | bitri 275 |
. . . 4
β’ ((π₯ = β¨π¦, π§β© β§ π¦ E π΄ β§ π§ E π΅) β (π₯ = β¨π¦, π§β© β§ (π¦ β π΄ β§ π§ β π΅))) |
15 | 14 | 2exbii 1852 |
. . 3
β’
(βπ¦βπ§(π₯ = β¨π¦, π§β© β§ π¦ E π΄ β§ π§ E π΅) β βπ¦βπ§(π₯ = β¨π¦, π§β© β§ (π¦ β π΄ β§ π§ β π΅))) |
16 | | vex 3448 |
. . . 4
β’ π₯ β V |
17 | 16, 4, 5 | brpprod3b 34518 |
. . 3
β’ (π₯pprod( E , E )β¨π΄, π΅β© β βπ¦βπ§(π₯ = β¨π¦, π§β© β§ π¦ E π΄ β§ π§ E π΅)) |
18 | | elxp 5657 |
. . 3
β’ (π₯ β (π΄ Γ π΅) β βπ¦βπ§(π₯ = β¨π¦, π§β© β§ (π¦ β π΄ β§ π§ β π΅))) |
19 | 15, 17, 18 | 3bitr4ri 304 |
. 2
β’ (π₯ β (π΄ Γ π΅) β π₯pprod( E , E )β¨π΄, π΅β©) |
20 | 1, 2, 3, 8, 19 | brtxpsd3 34527 |
1
β’
(β¨π΄, π΅β©CartπΆ β πΆ = (π΄ Γ π΅)) |