| Step | Hyp | Ref
| Expression |
|---|
| 1 | | 2onn 8638 |
. . . . . . . . . 10
β’
2o β Ο |
| 2 | | nnfi 9164 |
. . . . . . . . . 10
β’
(2o β Ο β 2o β
Fin) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . . . . 9
β’
2o β Fin |
| 4 | | enfi 9187 |
. . . . . . . . 9
β’ (π β 2o β
(π β Fin β
2o β Fin)) |
| 5 | 3, 4 | mpbiri 258 |
. . . . . . . 8
β’ (π β 2o β
π β
Fin) |
| 6 | 5 | adantl 483 |
. . . . . . 7
β’ ((π β π β§ π β 2o) β π β Fin) |
| 7 | | diffi 9176 |
. . . . . . 7
β’ (π β Fin β (π β {π}) β Fin) |
| 8 | 6, 7 | syl 17 |
. . . . . 6
β’ ((π β π β§ π β 2o) β (π β {π}) β Fin) |
| 9 | 8 | cardidd 10541 |
. . . . 5
β’ ((π β π β§ π β 2o) β
(cardβ(π β
{π})) β (π β {π})) |
| 10 | 9 | ensymd 8998 |
. . . 4
β’ ((π β π β§ π β 2o) β (π β {π}) β (cardβ(π β {π}))) |
| 11 | | simpl 484 |
. . . . . . 7
β’ ((π β π β§ π β 2o) β π β π) |
| 12 | | dif1card 10002 |
. . . . . . 7
β’ ((π β Fin β§ π β π) β (cardβπ) = suc (cardβ(π β {π}))) |
| 13 | 6, 11, 12 | syl2anc 585 |
. . . . . 6
β’ ((π β π β§ π β 2o) β
(cardβπ) = suc
(cardβ(π β
{π}))) |
| 14 | | cardennn 9975 |
. . . . . . . . 9
β’ ((π β 2o β§
2o β Ο) β (cardβπ) = 2o) |
| 15 | 1, 14 | mpan2 690 |
. . . . . . . 8
β’ (π β 2o β
(cardβπ) =
2o) |
| 16 | | df-2o 8464 |
. . . . . . . 8
β’
2o = suc 1o |
| 17 | 15, 16 | eqtrdi 2789 |
. . . . . . 7
β’ (π β 2o β
(cardβπ) = suc
1o) |
| 18 | 17 | adantl 483 |
. . . . . 6
β’ ((π β π β§ π β 2o) β
(cardβπ) = suc
1o) |
| 19 | 13, 18 | eqtr3d 2775 |
. . . . 5
β’ ((π β π β§ π β 2o) β suc
(cardβ(π β
{π})) = suc
1o) |
| 20 | | suc11reg 9611 |
. . . . 5
β’ (suc
(cardβ(π β
{π})) = suc 1o
β (cardβ(π
β {π})) =
1o) |
| 21 | 19, 20 | sylib 217 |
. . . 4
β’ ((π β π β§ π β 2o) β
(cardβ(π β
{π})) =
1o) |
| 22 | 10, 21 | breqtrd 5174 |
. . 3
β’ ((π β π β§ π β 2o) β (π β {π}) β 1o) |
| 23 | | en1 9018 |
. . 3
β’ ((π β {π}) β 1o β βπ₯(π β {π}) = {π₯}) |
| 24 | 22, 23 | sylib 217 |
. 2
β’ ((π β π β§ π β 2o) β βπ₯(π β {π}) = {π₯}) |
| 25 | | simplll 774 |
. . . . . . 7
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β π β π) |
| 26 | 25 | elexd 3495 |
. . . . . 6
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β π β V) |
| 27 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β (π β {π}) = {π₯}) |
| 28 | | sneqbg 4844 |
. . . . . . . . . . . . 13
β’ (π β π β ({π} = {π₯} β π = π₯)) |
| 29 | 28 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π β π β§ π = π₯) β {π} = {π₯}) |
| 30 | 29 | ad4ant14 751 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β {π} = {π₯}) |
| 31 | 27, 30 | eqtr4d 2776 |
. . . . . . . . . 10
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β (π β {π}) = {π}) |
| 32 | 31 | ineq2d 4212 |
. . . . . . . . 9
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β ({π} β© (π β {π})) = ({π} β© {π})) |
| 33 | | disjdif 4471 |
. . . . . . . . 9
β’ ({π} β© (π β {π})) = β
|
| 34 | | inidm 4218 |
. . . . . . . . 9
β’ ({π} β© {π}) = {π} |
| 35 | 32, 33, 34 | 3eqtr3g 2796 |
. . . . . . . 8
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β β
= {π}) |
| 36 | 35 | eqcomd 2739 |
. . . . . . 7
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β {π} = β
) |
| 37 | | snprc 4721 |
. . . . . . 7
β’ (Β¬
π β V β {π} = β
) |
| 38 | 36, 37 | sylibr 233 |
. . . . . 6
β’ ((((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β§ π = π₯) β Β¬ π β V) |
| 39 | 26, 38 | pm2.65da 816 |
. . . . 5
β’ (((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β Β¬ π = π₯) |
| 40 | 39 | neqned 2948 |
. . . 4
β’ (((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β π β π₯) |
| 41 | | simpr 486 |
. . . . . 6
β’ (((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β (π β {π}) = {π₯}) |
| 42 | 41 | unieqd 4922 |
. . . . 5
β’ (((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β βͺ (π β {π}) = βͺ {π₯}) |
| 43 | | unisnv 4931 |
. . . . 5
β’ βͺ {π₯}
= π₯ |
| 44 | 42, 43 | eqtrdi 2789 |
. . . 4
β’ (((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β βͺ (π β {π}) = π₯) |
| 45 | 40, 44 | neeqtrrd 3016 |
. . 3
β’ (((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β π β βͺ (π β {π})) |
| 46 | 45 | necomd 2997 |
. 2
β’ (((π β π β§ π β 2o) β§ (π β {π}) = {π₯}) β βͺ (π β {π}) β π) |
| 47 | 24, 46 | exlimddv 1939 |
1
β’ ((π β π β§ π β 2o) β βͺ (π
β {π}) β π) |
