Step | Hyp | Ref
| Expression |
1 | | pprodcnveq 34230 |
. . 3
β’
pprod(π
, π) = β‘pprod(β‘π
, β‘π) |
2 | 1 | breqi 5087 |
. 2
β’ (πpprod(π
, π)β¨π, πβ© β πβ‘pprod(β‘π
, β‘π)β¨π, πβ©) |
3 | | brpprod3.1 |
. . . . 5
β’ π β V |
4 | | opex 5392 |
. . . . 5
β’
β¨π, πβ© β V |
5 | 3, 4 | brcnv 5804 |
. . . 4
β’ (πβ‘pprod(β‘π
, β‘π)β¨π, πβ© β β¨π, πβ©pprod(β‘π
, β‘π)π) |
6 | | brpprod3.2 |
. . . . 5
β’ π β V |
7 | | brpprod3.3 |
. . . . 5
β’ π β V |
8 | 6, 7, 3 | brpprod3a 34233 |
. . . 4
β’
(β¨π, πβ©pprod(β‘π
, β‘π)π β βπ§βπ€(π = β¨π§, π€β© β§ πβ‘π
π§ β§ πβ‘ππ€)) |
9 | 5, 8 | bitri 275 |
. . 3
β’ (πβ‘pprod(β‘π
, β‘π)β¨π, πβ© β βπ§βπ€(π = β¨π§, π€β© β§ πβ‘π
π§ β§ πβ‘ππ€)) |
10 | | biid 261 |
. . . . 5
β’ (π = β¨π§, π€β© β π = β¨π§, π€β©) |
11 | | vex 3441 |
. . . . . 6
β’ π§ β V |
12 | 6, 11 | brcnv 5804 |
. . . . 5
β’ (πβ‘π
π§ β π§π
π) |
13 | | vex 3441 |
. . . . . 6
β’ π€ β V |
14 | 7, 13 | brcnv 5804 |
. . . . 5
β’ (πβ‘ππ€ β π€ππ) |
15 | 10, 12, 14 | 3anbi123i 1155 |
. . . 4
β’ ((π = β¨π§, π€β© β§ πβ‘π
π§ β§ πβ‘ππ€) β (π = β¨π§, π€β© β§ π§π
π β§ π€ππ)) |
16 | 15 | 2exbii 1849 |
. . 3
β’
(βπ§βπ€(π = β¨π§, π€β© β§ πβ‘π
π§ β§ πβ‘ππ€) β βπ§βπ€(π = β¨π§, π€β© β§ π§π
π β§ π€ππ)) |
17 | 9, 16 | bitri 275 |
. 2
β’ (πβ‘pprod(β‘π
, β‘π)β¨π, πβ© β βπ§βπ€(π = β¨π§, π€β© β§ π§π
π β§ π€ππ)) |
18 | 2, 17 | bitri 275 |
1
β’ (πpprod(π
, π)β¨π, πβ© β βπ§βπ€(π = β¨π§, π€β© β§ π§π
π β§ π€ππ)) |