This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 0fi ⊢ ∅ ∈ 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 ) )