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\prec 2_{𝑜}\leftrightarrow \left(A=\varnothing \vee A\approx 1_{𝑜}\right)$$

Proof

Step	Hyp	Ref	Expression
1		onfin2	$$⊢\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$$
2		inss2	$$⊢\mathrm{On}\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
3	1 2	eqsstri	$$⊢\mathrm{\omega }\subseteq \mathrm{Fin}$$
4		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
5	3 4	sselii	$$⊢2_{𝑜}\in \mathrm{Fin}$$
6		sdomdom	$$⊢A\prec 2_{𝑜}\to A\preccurlyeq 2_{𝑜}$$
7		domfi	$$⊢\left(2_{𝑜}\in \mathrm{Fin}\wedge A\preccurlyeq 2_{𝑜}\right)\to A\in \mathrm{Fin}$$
8	5 6 7	sylancr	$$⊢A\prec 2_{𝑜}\to A\in \mathrm{Fin}$$
9		id	$$⊢A=\varnothing \to A=\varnothing$$
10		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
11	9 10	eqeltrdi	$$⊢A=\varnothing \to A\in \mathrm{Fin}$$
12		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
13	3 12	sselii	$$⊢1_{𝑜}\in \mathrm{Fin}$$
14		enfi	$$⊢A\approx 1_{𝑜}\to \left(A\in \mathrm{Fin}\leftrightarrow 1_{𝑜}\in \mathrm{Fin}\right)$$
15	13 14	mpbiri	$$⊢A\approx 1_{𝑜}\to A\in \mathrm{Fin}$$
16	11 15	jaoi	$$⊢\left(A=\varnothing \vee A\approx 1_{𝑜}\right)\to A\in \mathrm{Fin}$$
17		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
18	17	eleq2i	$$⊢\mathrm{card}\left(A\right)\in 2_{𝑜}\leftrightarrow \mathrm{card}\left(A\right)\in \left\{\varnothing ,1_{𝑜}\right\}$$
19		fvex	$$⊢\mathrm{card}\left(A\right)\in \mathrm{V}$$
20	19	elpr	$$⊢\mathrm{card}\left(A\right)\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(\mathrm{card}\left(A\right)=\varnothing \vee \mathrm{card}\left(A\right)=1_{𝑜}\right)$$
21	18 20	bitri	$$⊢\mathrm{card}\left(A\right)\in 2_{𝑜}\leftrightarrow \left(\mathrm{card}\left(A\right)=\varnothing \vee \mathrm{card}\left(A\right)=1_{𝑜}\right)$$
22	21	a1i	$$⊢A\in \mathrm{Fin}\to \left(\mathrm{card}\left(A\right)\in 2_{𝑜}\leftrightarrow \left(\mathrm{card}\left(A\right)=\varnothing \vee \mathrm{card}\left(A\right)=1_{𝑜}\right)\right)$$
23		cardnn	$$⊢2_{𝑜}\in \mathrm{\omega }\to \mathrm{card}\left(2_{𝑜}\right)=2_{𝑜}$$
24	4 23	ax-mp	$$⊢\mathrm{card}\left(2_{𝑜}\right)=2_{𝑜}$$
25	24	eleq2i	$$⊢\mathrm{card}\left(A\right)\in \mathrm{card}\left(2_{𝑜}\right)\leftrightarrow \mathrm{card}\left(A\right)\in 2_{𝑜}$$
26		finnum	$$⊢A\in \mathrm{Fin}\to A\in \mathrm{dom}\mathrm{card}$$
27		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
28		onenon	$$⊢2_{𝑜}\in \mathrm{On}\to 2_{𝑜}\in \mathrm{dom}\mathrm{card}$$
29	27 28	ax-mp	$$⊢2_{𝑜}\in \mathrm{dom}\mathrm{card}$$
30		cardsdom2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge 2_{𝑜}\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left(A\right)\in \mathrm{card}\left(2_{𝑜}\right)\leftrightarrow A\prec 2_{𝑜}\right)$$
31	26 29 30	sylancl	$$⊢A\in \mathrm{Fin}\to \left(\mathrm{card}\left(A\right)\in \mathrm{card}\left(2_{𝑜}\right)\leftrightarrow A\prec 2_{𝑜}\right)$$
32	25 31	bitr3id	$$⊢A\in \mathrm{Fin}\to \left(\mathrm{card}\left(A\right)\in 2_{𝑜}\leftrightarrow A\prec 2_{𝑜}\right)$$
33		cardnueq0	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\mathrm{card}\left(A\right)=\varnothing \leftrightarrow A=\varnothing \right)$$
34	26 33	syl	$$⊢A\in \mathrm{Fin}\to \left(\mathrm{card}\left(A\right)=\varnothing \leftrightarrow A=\varnothing \right)$$
35		cardnn	$$⊢1_{𝑜}\in \mathrm{\omega }\to \mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
36	12 35	ax-mp	$$⊢\mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
37	36	eqeq2i	$$⊢\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow \mathrm{card}\left(A\right)=1_{𝑜}$$
38		finnum	$$⊢1_{𝑜}\in \mathrm{Fin}\to 1_{𝑜}\in \mathrm{dom}\mathrm{card}$$
39	13 38	ax-mp	$$⊢1_{𝑜}\in \mathrm{dom}\mathrm{card}$$
40		carden2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge 1_{𝑜}\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow A\approx 1_{𝑜}\right)$$
41	26 39 40	sylancl	$$⊢A\in \mathrm{Fin}\to \left(\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow A\approx 1_{𝑜}\right)$$
42	37 41	bitr3id	$$⊢A\in \mathrm{Fin}\to \left(\mathrm{card}\left(A\right)=1_{𝑜}\leftrightarrow A\approx 1_{𝑜}\right)$$
43	34 42	orbi12d	$$⊢A\in \mathrm{Fin}\to \left(\left(\mathrm{card}\left(A\right)=\varnothing \vee \mathrm{card}\left(A\right)=1_{𝑜}\right)\leftrightarrow \left(A=\varnothing \vee A\approx 1_{𝑜}\right)\right)$$
44	22 32 43	3bitr3d	$$⊢A\in \mathrm{Fin}\to \left(A\prec 2_{𝑜}\leftrightarrow \left(A=\varnothing \vee A\approx 1_{𝑜}\right)\right)$$
45	8 16 44	pm5.21nii	$$⊢A\prec 2_{𝑜}\leftrightarrow \left(A=\varnothing \vee A\approx 1_{𝑜}\right)$$