Metamath Proof Explorer

Theorem sdom2en01

Description: A set with less than two elements has 0 or 1. (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Assertion sdom2en01 
|- ( A ~< 2o <-> ( A = (/) \/ A ~~ 1o ) )

Proof

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 ) )