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