Step | Hyp | Ref
| Expression |
1 | | djur 7068 |
. . 3
β’ (π₯ β (π΄ β π΅) β (βπ¦ β π΄ π₯ = (inlβπ¦) β¨ βπ¦ β π΅ π₯ = (inrβπ¦))) |
2 | | simpr 110 |
. . . . . . 7
β’ ((π¦ β π΄ β§ π₯ = (inlβπ¦)) β π₯ = (inlβπ¦)) |
3 | | df-inl 7046 |
. . . . . . . . 9
β’ inl =
(π₯ β V β¦
β¨β
, π₯β©) |
4 | | opeq2 3780 |
. . . . . . . . 9
β’ (π₯ = π¦ β β¨β
, π₯β© = β¨β
, π¦β©) |
5 | | elex 2749 |
. . . . . . . . 9
β’ (π¦ β π΄ β π¦ β V) |
6 | | 0ex 4131 |
. . . . . . . . . . 11
β’ β
β V |
7 | | vex 2741 |
. . . . . . . . . . 11
β’ π¦ β V |
8 | 6, 7 | opex 4230 |
. . . . . . . . . 10
β’
β¨β
, π¦β© β V |
9 | 8 | a1i 9 |
. . . . . . . . 9
β’ (π¦ β π΄ β β¨β
, π¦β© β V) |
10 | 3, 4, 5, 9 | fvmptd3 5610 |
. . . . . . . 8
β’ (π¦ β π΄ β (inlβπ¦) = β¨β
, π¦β©) |
11 | 10 | adantr 276 |
. . . . . . 7
β’ ((π¦ β π΄ β§ π₯ = (inlβπ¦)) β (inlβπ¦) = β¨β
, π¦β©) |
12 | 2, 11 | eqtrd 2210 |
. . . . . 6
β’ ((π¦ β π΄ β§ π₯ = (inlβπ¦)) β π₯ = β¨β
, π¦β©) |
13 | | elun1 3303 |
. . . . . . . . 9
β’ (π¦ β π΄ β π¦ β (π΄ βͺ π΅)) |
14 | 6 | prid1 3699 |
. . . . . . . . 9
β’ β
β {β
, 1o} |
15 | 13, 14 | jctil 312 |
. . . . . . . 8
β’ (π¦ β π΄ β (β
β {β
,
1o} β§ π¦
β (π΄ βͺ π΅))) |
16 | 15 | adantr 276 |
. . . . . . 7
β’ ((π¦ β π΄ β§ π₯ = (inlβπ¦)) β (β
β {β
,
1o} β§ π¦
β (π΄ βͺ π΅))) |
17 | | opelxp 4657 |
. . . . . . 7
β’
(β¨β
, π¦β© β ({β
, 1o}
Γ (π΄ βͺ π΅)) β (β
β
{β
, 1o} β§ π¦ β (π΄ βͺ π΅))) |
18 | 16, 17 | sylibr 134 |
. . . . . 6
β’ ((π¦ β π΄ β§ π₯ = (inlβπ¦)) β β¨β
, π¦β© β ({β
, 1o}
Γ (π΄ βͺ π΅))) |
19 | 12, 18 | eqeltrd 2254 |
. . . . 5
β’ ((π¦ β π΄ β§ π₯ = (inlβπ¦)) β π₯ β ({β
, 1o} Γ
(π΄ βͺ π΅))) |
20 | 19 | rexlimiva 2589 |
. . . 4
β’
(βπ¦ β
π΄ π₯ = (inlβπ¦) β π₯ β ({β
, 1o} Γ
(π΄ βͺ π΅))) |
21 | | simpr 110 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π₯ = (inrβπ¦)) β π₯ = (inrβπ¦)) |
22 | | df-inr 7047 |
. . . . . . . . 9
β’ inr =
(π₯ β V β¦
β¨1o, π₯β©) |
23 | | opeq2 3780 |
. . . . . . . . 9
β’ (π₯ = π¦ β β¨1o, π₯β© = β¨1o,
π¦β©) |
24 | | elex 2749 |
. . . . . . . . 9
β’ (π¦ β π΅ β π¦ β V) |
25 | | 1oex 6425 |
. . . . . . . . . . 11
β’
1o β V |
26 | 25, 7 | opex 4230 |
. . . . . . . . . 10
β’
β¨1o, π¦β© β V |
27 | 26 | a1i 9 |
. . . . . . . . 9
β’ (π¦ β π΅ β β¨1o, π¦β© β
V) |
28 | 22, 23, 24, 27 | fvmptd3 5610 |
. . . . . . . 8
β’ (π¦ β π΅ β (inrβπ¦) = β¨1o, π¦β©) |
29 | 28 | adantr 276 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π₯ = (inrβπ¦)) β (inrβπ¦) = β¨1o, π¦β©) |
30 | 21, 29 | eqtrd 2210 |
. . . . . 6
β’ ((π¦ β π΅ β§ π₯ = (inrβπ¦)) β π₯ = β¨1o, π¦β©) |
31 | | elun2 3304 |
. . . . . . . . 9
β’ (π¦ β π΅ β π¦ β (π΄ βͺ π΅)) |
32 | 31 | adantr 276 |
. . . . . . . 8
β’ ((π¦ β π΅ β§ π₯ = (inrβπ¦)) β π¦ β (π΄ βͺ π΅)) |
33 | 25 | prid2 3700 |
. . . . . . . 8
β’
1o β {β
, 1o} |
34 | 32, 33 | jctil 312 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π₯ = (inrβπ¦)) β (1o β {β
,
1o} β§ π¦
β (π΄ βͺ π΅))) |
35 | | opelxp 4657 |
. . . . . . 7
β’
(β¨1o, π¦β© β ({β
, 1o}
Γ (π΄ βͺ π΅)) β (1o β
{β
, 1o} β§ π¦ β (π΄ βͺ π΅))) |
36 | 34, 35 | sylibr 134 |
. . . . . 6
β’ ((π¦ β π΅ β§ π₯ = (inrβπ¦)) β β¨1o, π¦β© β ({β
,
1o} Γ (π΄
βͺ π΅))) |
37 | 30, 36 | eqeltrd 2254 |
. . . . 5
β’ ((π¦ β π΅ β§ π₯ = (inrβπ¦)) β π₯ β ({β
, 1o} Γ
(π΄ βͺ π΅))) |
38 | 37 | rexlimiva 2589 |
. . . 4
β’
(βπ¦ β
π΅ π₯ = (inrβπ¦) β π₯ β ({β
, 1o} Γ
(π΄ βͺ π΅))) |
39 | 20, 38 | jaoi 716 |
. . 3
β’
((βπ¦ β
π΄ π₯ = (inlβπ¦) β¨ βπ¦ β π΅ π₯ = (inrβπ¦)) β π₯ β ({β
, 1o} Γ
(π΄ βͺ π΅))) |
40 | 1, 39 | sylbi 121 |
. 2
β’ (π₯ β (π΄ β π΅) β π₯ β ({β
, 1o} Γ
(π΄ βͺ π΅))) |
41 | 40 | ssriv 3160 |
1
β’ (π΄ β π΅) β ({β
, 1o} Γ
(π΄ βͺ π΅)) |