Step | Hyp | Ref
| Expression |
1 | | relxp 5655 |
. . 3
β’ Rel
(π Γ π) |
2 | | txuni2.1 |
. . . . . . . 8
β’ π = βͺ
π
|
3 | 2 | eleq2i 2826 |
. . . . . . 7
β’ (π§ β π β π§ β βͺ π
) |
4 | | eluni2 4873 |
. . . . . . 7
β’ (π§ β βͺ π
β βπ β
π
π§ β π) |
5 | 3, 4 | bitri 275 |
. . . . . 6
β’ (π§ β π β βπ β π
π§ β π) |
6 | | txuni2.2 |
. . . . . . . 8
β’ π = βͺ
π |
7 | 6 | eleq2i 2826 |
. . . . . . 7
β’ (π€ β π β π€ β βͺ π) |
8 | | eluni2 4873 |
. . . . . . 7
β’ (π€ β βͺ π
β βπ β
π π€ β π ) |
9 | 7, 8 | bitri 275 |
. . . . . 6
β’ (π€ β π β βπ β π π€ β π ) |
10 | 5, 9 | anbi12i 628 |
. . . . 5
β’ ((π§ β π β§ π€ β π) β (βπ β π
π§ β π β§ βπ β π π€ β π )) |
11 | | opelxp 5673 |
. . . . 5
β’
(β¨π§, π€β© β (π Γ π) β (π§ β π β§ π€ β π)) |
12 | | reeanv 3216 |
. . . . 5
β’
(βπ β
π
βπ β π (π§ β π β§ π€ β π ) β (βπ β π
π§ β π β§ βπ β π π€ β π )) |
13 | 10, 11, 12 | 3bitr4i 303 |
. . . 4
β’
(β¨π§, π€β© β (π Γ π) β βπ β π
βπ β π (π§ β π β§ π€ β π )) |
14 | | opelxp 5673 |
. . . . . 6
β’
(β¨π§, π€β© β (π Γ π ) β (π§ β π β§ π€ β π )) |
15 | | eqid 2733 |
. . . . . . . . . 10
β’ (π Γ π ) = (π Γ π ) |
16 | | xpeq1 5651 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ Γ π¦) = (π Γ π¦)) |
17 | 16 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π Γ π ) = (π₯ Γ π¦) β (π Γ π ) = (π Γ π¦))) |
18 | | xpeq2 5658 |
. . . . . . . . . . . 12
β’ (π¦ = π β (π Γ π¦) = (π Γ π )) |
19 | 18 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π¦ = π β ((π Γ π ) = (π Γ π¦) β (π Γ π ) = (π Γ π ))) |
20 | 17, 19 | rspc2ev 3594 |
. . . . . . . . . 10
β’ ((π β π
β§ π β π β§ (π Γ π ) = (π Γ π )) β βπ₯ β π
βπ¦ β π (π Γ π ) = (π₯ Γ π¦)) |
21 | 15, 20 | mp3an3 1451 |
. . . . . . . . 9
β’ ((π β π
β§ π β π) β βπ₯ β π
βπ¦ β π (π Γ π ) = (π₯ Γ π¦)) |
22 | | vex 3451 |
. . . . . . . . . . 11
β’ π β V |
23 | | vex 3451 |
. . . . . . . . . . 11
β’ π β V |
24 | 22, 23 | xpex 7691 |
. . . . . . . . . 10
β’ (π Γ π ) β V |
25 | | eqeq1 2737 |
. . . . . . . . . . 11
β’ (π§ = (π Γ π ) β (π§ = (π₯ Γ π¦) β (π Γ π ) = (π₯ Γ π¦))) |
26 | 25 | 2rexbidv 3210 |
. . . . . . . . . 10
β’ (π§ = (π Γ π ) β (βπ₯ β π
βπ¦ β π π§ = (π₯ Γ π¦) β βπ₯ β π
βπ¦ β π (π Γ π ) = (π₯ Γ π¦))) |
27 | | txval.1 |
. . . . . . . . . . 11
β’ π΅ = ran (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)) |
28 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)) = (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)) |
29 | 28 | rnmpo 7493 |
. . . . . . . . . . 11
β’ ran
(π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)) = {π§ β£ βπ₯ β π
βπ¦ β π π§ = (π₯ Γ π¦)} |
30 | 27, 29 | eqtri 2761 |
. . . . . . . . . 10
β’ π΅ = {π§ β£ βπ₯ β π
βπ¦ β π π§ = (π₯ Γ π¦)} |
31 | 24, 26, 30 | elab2 3638 |
. . . . . . . . 9
β’ ((π Γ π ) β π΅ β βπ₯ β π
βπ¦ β π (π Γ π ) = (π₯ Γ π¦)) |
32 | 21, 31 | sylibr 233 |
. . . . . . . 8
β’ ((π β π
β§ π β π) β (π Γ π ) β π΅) |
33 | | elssuni 4902 |
. . . . . . . 8
β’ ((π Γ π ) β π΅ β (π Γ π ) β βͺ π΅) |
34 | 32, 33 | syl 17 |
. . . . . . 7
β’ ((π β π
β§ π β π) β (π Γ π ) β βͺ π΅) |
35 | 34 | sseld 3947 |
. . . . . 6
β’ ((π β π
β§ π β π) β (β¨π§, π€β© β (π Γ π ) β β¨π§, π€β© β βͺ
π΅)) |
36 | 14, 35 | biimtrrid 242 |
. . . . 5
β’ ((π β π
β§ π β π) β ((π§ β π β§ π€ β π ) β β¨π§, π€β© β βͺ
π΅)) |
37 | 36 | rexlimivv 3193 |
. . . 4
β’
(βπ β
π
βπ β π (π§ β π β§ π€ β π ) β β¨π§, π€β© β βͺ
π΅) |
38 | 13, 37 | sylbi 216 |
. . 3
β’
(β¨π§, π€β© β (π Γ π) β β¨π§, π€β© β βͺ
π΅) |
39 | 1, 38 | relssi 5747 |
. 2
β’ (π Γ π) β βͺ π΅ |
40 | | elssuni 4902 |
. . . . . . . . . 10
β’ (π₯ β π
β π₯ β βͺ π
) |
41 | 40, 2 | sseqtrrdi 3999 |
. . . . . . . . 9
β’ (π₯ β π
β π₯ β π) |
42 | | elssuni 4902 |
. . . . . . . . . 10
β’ (π¦ β π β π¦ β βͺ π) |
43 | 42, 6 | sseqtrrdi 3999 |
. . . . . . . . 9
β’ (π¦ β π β π¦ β π) |
44 | | xpss12 5652 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π) β (π₯ Γ π¦) β (π Γ π)) |
45 | 41, 43, 44 | syl2an 597 |
. . . . . . . 8
β’ ((π₯ β π
β§ π¦ β π) β (π₯ Γ π¦) β (π Γ π)) |
46 | | vex 3451 |
. . . . . . . . . 10
β’ π₯ β V |
47 | | vex 3451 |
. . . . . . . . . 10
β’ π¦ β V |
48 | 46, 47 | xpex 7691 |
. . . . . . . . 9
β’ (π₯ Γ π¦) β V |
49 | 48 | elpw 4568 |
. . . . . . . 8
β’ ((π₯ Γ π¦) β π« (π Γ π) β (π₯ Γ π¦) β (π Γ π)) |
50 | 45, 49 | sylibr 233 |
. . . . . . 7
β’ ((π₯ β π
β§ π¦ β π) β (π₯ Γ π¦) β π« (π Γ π)) |
51 | 50 | rgen2 3191 |
. . . . . 6
β’
βπ₯ β
π
βπ¦ β π (π₯ Γ π¦) β π« (π Γ π) |
52 | 28 | fmpo 8004 |
. . . . . 6
β’
(βπ₯ β
π
βπ¦ β π (π₯ Γ π¦) β π« (π Γ π) β (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)):(π
Γ π)βΆπ« (π Γ π)) |
53 | 51, 52 | mpbi 229 |
. . . . 5
β’ (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)):(π
Γ π)βΆπ« (π Γ π) |
54 | | frn 6679 |
. . . . 5
β’ ((π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)):(π
Γ π)βΆπ« (π Γ π) β ran (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)) β π« (π Γ π)) |
55 | 53, 54 | ax-mp 5 |
. . . 4
β’ ran
(π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)) β π« (π Γ π) |
56 | 27, 55 | eqsstri 3982 |
. . 3
β’ π΅ β π« (π Γ π) |
57 | | sspwuni 5064 |
. . 3
β’ (π΅ β π« (π Γ π) β βͺ π΅ β (π Γ π)) |
58 | 56, 57 | mpbi 229 |
. 2
β’ βͺ π΅
β (π Γ π) |
59 | 39, 58 | eqssi 3964 |
1
β’ (π Γ π) = βͺ π΅ |