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≺2𝑜↔A=∅∨A≈1𝑜

Proof

Step Hyp Ref Expression
1 onfin2 ⊢ω=On∩Fin
2 inss2 ⊢On∩Fin⊆Fin
3 1 2 eqsstri ⊢ω⊆Fin
4 2onn ⊢2𝑜∈ω
5 3 4 sselii ⊢2𝑜∈Fin
6 sdomdom ⊢A≺2𝑜→A≼2𝑜
7 domfi ⊢2𝑜∈Fin∧A≼2𝑜→A∈Fin
8 5 6 7 sylancr ⊢A≺2𝑜→A∈Fin
9 id ⊢A=∅→A=∅
10 0fin ⊢∅∈Fin
11 9 10 eqeltrdi ⊢A=∅→A∈Fin
12 1onn ⊢1𝑜∈ω
13 3 12 sselii ⊢1𝑜∈Fin
14 enfi ⊢A≈1𝑜→A∈Fin↔1𝑜∈Fin
15 13 14 mpbiri ⊢A≈1𝑜→A∈Fin
16 11 15 jaoi ⊢A=∅∨A≈1𝑜→A∈Fin
17 df2o3 ⊢2𝑜=∅1𝑜
18 17 eleq2i ⊢card⁡A∈2𝑜↔card⁡A∈∅1𝑜
19 fvex ⊢card⁡A∈V
20 19 elpr ⊢card⁡A∈∅1𝑜↔card⁡A=∅∨card⁡A=1𝑜
21 18 20 bitri ⊢card⁡A∈2𝑜↔card⁡A=∅∨card⁡A=1𝑜
22 21 a1i ⊢A∈Fin→card⁡A∈2𝑜↔card⁡A=∅∨card⁡A=1𝑜
23 cardnn ⊢2𝑜∈ω→card⁡2𝑜=2𝑜
24 4 23 ax-mp ⊢card⁡2𝑜=2𝑜
25 24 eleq2i ⊢card⁡A∈card⁡2𝑜↔card⁡A∈2𝑜
26 finnum ⊢A∈Fin→A∈dom⁡card
27 2on ⊢2𝑜∈On
28 onenon ⊢2𝑜∈On→2𝑜∈dom⁡card
29 27 28 ax-mp ⊢2𝑜∈dom⁡card
30 cardsdom2 ⊢A∈dom⁡card∧2𝑜∈dom⁡card→card⁡A∈card⁡2𝑜↔A≺2𝑜
31 26 29 30 sylancl ⊢A∈Fin→card⁡A∈card⁡2𝑜↔A≺2𝑜
32 25 31 bitr3id ⊢A∈Fin→card⁡A∈2𝑜↔A≺2𝑜
33 cardnueq0 ⊢A∈dom⁡card→card⁡A=∅↔A=∅
34 26 33 syl ⊢A∈Fin→card⁡A=∅↔A=∅
35 cardnn ⊢1𝑜∈ω→card⁡1𝑜=1𝑜
36 12 35 ax-mp ⊢card⁡1𝑜=1𝑜
37 36 eqeq2i ⊢card⁡A=card⁡1𝑜↔card⁡A=1𝑜
38 finnum ⊢1𝑜∈Fin→1𝑜∈dom⁡card
39 13 38 ax-mp ⊢1𝑜∈dom⁡card
40 carden2 ⊢A∈dom⁡card∧1𝑜∈dom⁡card→card⁡A=card⁡1𝑜↔A≈1𝑜
41 26 39 40 sylancl ⊢A∈Fin→card⁡A=card⁡1𝑜↔A≈1𝑜
42 37 41 bitr3id ⊢A∈Fin→card⁡A=1𝑜↔A≈1𝑜
43 34 42 orbi12d ⊢A∈Fin→card⁡A=∅∨card⁡A=1𝑜↔A=∅∨A≈1𝑜
44 22 32 43 3bitr3d ⊢A∈Fin→A≺2𝑜↔A=∅∨A≈1𝑜
45 8 16 44 pm5.21nii ⊢A≺2𝑜↔A=∅∨A≈1𝑜