| Step |
Hyp |
Ref |
Expression |
| 1 |
|
onfin2 |
|- _om = ( On i^i Fin ) |
| 2 |
|
inss2 |
|- ( On i^i Fin ) C_ Fin |
| 3 |
1 2
|
eqsstri |
|- _om C_ Fin |
| 4 |
|
2onn |
|- 2o e. _om |
| 5 |
3 4
|
sselii |
|- 2o e. Fin |
| 6 |
|
sdomdom |
|- ( A ~< 2o -> A ~<_ 2o ) |
| 7 |
|
domfi |
|- ( ( 2o e. Fin /\ A ~<_ 2o ) -> A e. Fin ) |
| 8 |
5 6 7
|
sylancr |
|- ( A ~< 2o -> A e. Fin ) |
| 9 |
|
id |
|- ( A = (/) -> A = (/) ) |
| 10 |
|
0fi |
|- (/) e. Fin |
| 11 |
9 10
|
eqeltrdi |
|- ( A = (/) -> A e. Fin ) |
| 12 |
|
1onn |
|- 1o e. _om |
| 13 |
3 12
|
sselii |
|- 1o e. Fin |
| 14 |
|
enfi |
|- ( A ~~ 1o -> ( A e. Fin <-> 1o e. Fin ) ) |
| 15 |
13 14
|
mpbiri |
|- ( A ~~ 1o -> A e. Fin ) |
| 16 |
11 15
|
jaoi |
|- ( ( A = (/) \/ A ~~ 1o ) -> A e. Fin ) |
| 17 |
|
df2o3 |
|- 2o = { (/) , 1o } |
| 18 |
17
|
eleq2i |
|- ( ( card ` A ) e. 2o <-> ( card ` A ) e. { (/) , 1o } ) |
| 19 |
|
fvex |
|- ( card ` A ) e. _V |
| 20 |
19
|
elpr |
|- ( ( card ` A ) e. { (/) , 1o } <-> ( ( card ` A ) = (/) \/ ( card ` A ) = 1o ) ) |
| 21 |
18 20
|
bitri |
|- ( ( card ` A ) e. 2o <-> ( ( card ` A ) = (/) \/ ( card ` A ) = 1o ) ) |
| 22 |
21
|
a1i |
|- ( A e. Fin -> ( ( card ` A ) e. 2o <-> ( ( card ` A ) = (/) \/ ( card ` A ) = 1o ) ) ) |
| 23 |
|
cardnn |
|- ( 2o e. _om -> ( card ` 2o ) = 2o ) |
| 24 |
4 23
|
ax-mp |
|- ( card ` 2o ) = 2o |
| 25 |
24
|
eleq2i |
|- ( ( card ` A ) e. ( card ` 2o ) <-> ( card ` A ) e. 2o ) |
| 26 |
|
finnum |
|- ( A e. Fin -> A e. dom card ) |
| 27 |
|
2on |
|- 2o e. On |
| 28 |
|
onenon |
|- ( 2o e. On -> 2o e. dom card ) |
| 29 |
27 28
|
ax-mp |
|- 2o e. dom card |
| 30 |
|
cardsdom2 |
|- ( ( A e. dom card /\ 2o e. dom card ) -> ( ( card ` A ) e. ( card ` 2o ) <-> A ~< 2o ) ) |
| 31 |
26 29 30
|
sylancl |
|- ( A e. Fin -> ( ( card ` A ) e. ( card ` 2o ) <-> A ~< 2o ) ) |
| 32 |
25 31
|
bitr3id |
|- ( A e. Fin -> ( ( card ` A ) e. 2o <-> A ~< 2o ) ) |
| 33 |
|
cardnueq0 |
|- ( A e. dom card -> ( ( card ` A ) = (/) <-> A = (/) ) ) |
| 34 |
26 33
|
syl |
|- ( A e. Fin -> ( ( card ` A ) = (/) <-> A = (/) ) ) |
| 35 |
|
cardnn |
|- ( 1o e. _om -> ( card ` 1o ) = 1o ) |
| 36 |
12 35
|
ax-mp |
|- ( card ` 1o ) = 1o |
| 37 |
36
|
eqeq2i |
|- ( ( card ` A ) = ( card ` 1o ) <-> ( card ` A ) = 1o ) |
| 38 |
|
finnum |
|- ( 1o e. Fin -> 1o e. dom card ) |
| 39 |
13 38
|
ax-mp |
|- 1o e. dom card |
| 40 |
|
carden2 |
|- ( ( A e. dom card /\ 1o e. dom card ) -> ( ( card ` A ) = ( card ` 1o ) <-> A ~~ 1o ) ) |
| 41 |
26 39 40
|
sylancl |
|- ( A e. Fin -> ( ( card ` A ) = ( card ` 1o ) <-> A ~~ 1o ) ) |
| 42 |
37 41
|
bitr3id |
|- ( A e. Fin -> ( ( card ` A ) = 1o <-> A ~~ 1o ) ) |
| 43 |
34 42
|
orbi12d |
|- ( A e. Fin -> ( ( ( card ` A ) = (/) \/ ( card ` A ) = 1o ) <-> ( A = (/) \/ A ~~ 1o ) ) ) |
| 44 |
22 32 43
|
3bitr3d |
|- ( A e. Fin -> ( A ~< 2o <-> ( A = (/) \/ A ~~ 1o ) ) ) |
| 45 |
8 16 44
|
pm5.21nii |
|- ( A ~< 2o <-> ( A = (/) \/ A ~~ 1o ) ) |