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 ( 𝐴 ≺ 2o ↔ ( 𝐴 = ∅ ∨ 𝐴 ≈ 1o ) )

Proof

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