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 𝑜