Theorem 1sdom

Description: A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom .) (Contributed by Mario Carneiro, 12-Jan-2013)

	Ref	Expression
Assertion	1sdom	$$⊢A\in V\to \left(1_{𝑜}\prec A\leftrightarrow \exists x\in A\exists y\in A\neg x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢a=A\to \left(1_{𝑜}\prec a\leftrightarrow 1_{𝑜}\prec A\right)$$
2		rexeq	$$⊢a=A\to \left(\exists y\in a\neg x=y\leftrightarrow \exists y\in A\neg x=y\right)$$
3	2	rexeqbi1dv	$$⊢a=A\to \left(\exists x\in a\exists y\in a\neg x=y\leftrightarrow \exists x\in A\exists y\in A\neg x=y\right)$$
4		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
5		sucdom	$$⊢1_{𝑜}\in \mathrm{\omega }\to \left(1_{𝑜}\prec a\leftrightarrow \mathrm{suc}{1}_{𝑜}\preccurlyeq a\right)$$
6	4 5	ax-mp	$$⊢1_{𝑜}\prec a\leftrightarrow \mathrm{suc}{1}_{𝑜}\preccurlyeq a$$
7		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
8	7	breq1i	$$⊢2_{𝑜}\preccurlyeq a\leftrightarrow \mathrm{suc}{1}_{𝑜}\preccurlyeq a$$
9		2dom	$$⊢2_{𝑜}\preccurlyeq a\to \exists x\in a\exists y\in a\neg x=y$$
10		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
11		vex	$$⊢x\in \mathrm{V}$$
12		vex	$$⊢y\in \mathrm{V}$$
13		0ex	$$⊢\varnothing \in \mathrm{V}$$
14		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
15	11 12 13 14	funpr	$$⊢x\ne y\to \mathrm{Fun}\left\{⟨x,\varnothing ⟩,⟨y,1_{𝑜}⟩\right\}$$
16		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
17		1n0	$$⊢1_{𝑜}\ne \varnothing$$
18	17	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
19	13 14 11 12	fpr	$$⊢\varnothing \ne 1_{𝑜}\to \left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}⟶\left\{x,y\right\}$$
20	18 19	ax-mp	$$⊢\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}⟶\left\{x,y\right\}$$
21		df-f1	$$⊢\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}\left\{x,y\right\}\leftrightarrow \left(\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}⟶\left\{x,y\right\}\wedge \mathrm{Fun}{\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}}^{-1}\right)$$
22	20 21	mpbiran	$$⊢\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}\left\{x,y\right\}\leftrightarrow \mathrm{Fun}{\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}}^{-1}$$
23	13 11	cnvsn	$$⊢{\left\{⟨\varnothing ,x⟩\right\}}^{-1}=\left\{⟨x,\varnothing ⟩\right\}$$
24	14 12	cnvsn	$$⊢{\left\{⟨1_{𝑜},y⟩\right\}}^{-1}=\left\{⟨y,1_{𝑜}⟩\right\}$$
25	23 24	uneq12i	$$⊢{\left\{⟨\varnothing ,x⟩\right\}}^{-1}\cup {\left\{⟨1_{𝑜},y⟩\right\}}^{-1}=\left\{⟨x,\varnothing ⟩\right\}\cup \left\{⟨y,1_{𝑜}⟩\right\}$$
26		df-pr	$$⊢\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}=\left\{⟨\varnothing ,x⟩\right\}\cup \left\{⟨1_{𝑜},y⟩\right\}$$
27	26	cnveqi	$$⊢{\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}}^{-1}={\left(\left\{⟨\varnothing ,x⟩\right\}\cup \left\{⟨1_{𝑜},y⟩\right\}\right)}^{-1}$$
28		cnvun	$$⊢{\left(\left\{⟨\varnothing ,x⟩\right\}\cup \left\{⟨1_{𝑜},y⟩\right\}\right)}^{-1}={\left\{⟨\varnothing ,x⟩\right\}}^{-1}\cup {\left\{⟨1_{𝑜},y⟩\right\}}^{-1}$$
29	27 28	eqtri	$$⊢{\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}}^{-1}={\left\{⟨\varnothing ,x⟩\right\}}^{-1}\cup {\left\{⟨1_{𝑜},y⟩\right\}}^{-1}$$
30		df-pr	$$⊢\left\{⟨x,\varnothing ⟩,⟨y,1_{𝑜}⟩\right\}=\left\{⟨x,\varnothing ⟩\right\}\cup \left\{⟨y,1_{𝑜}⟩\right\}$$
31	25 29 30	3eqtr4i	$$⊢{\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}}^{-1}=\left\{⟨x,\varnothing ⟩,⟨y,1_{𝑜}⟩\right\}$$
32	31	funeqi	$$⊢\mathrm{Fun}{\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}}^{-1}\leftrightarrow \mathrm{Fun}\left\{⟨x,\varnothing ⟩,⟨y,1_{𝑜}⟩\right\}$$
33	22 32	bitr2i	$$⊢\mathrm{Fun}\left\{⟨x,\varnothing ⟩,⟨y,1_{𝑜}⟩\right\}\leftrightarrow \left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}\left\{x,y\right\}$$
34	15 16 33	3imtr3i	$$⊢\neg x=y\to \left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}\left\{x,y\right\}$$
35		prssi	$$⊢\left(x\in a\wedge y\in a\right)\to \left\{x,y\right\}\subseteq a$$
36		f1ss	$$⊢\left(\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}\left\{x,y\right\}\wedge \left\{x,y\right\}\subseteq a\right)\to \left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a$$
37	34 35 36	syl2an	$$⊢\left(\neg x=y\wedge \left(x\in a\wedge y\in a\right)\right)\to \left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a$$
38		prex	$$⊢\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\in \mathrm{V}$$
39		f1eq1	$$⊢f=\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\to \left(f:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a\leftrightarrow \left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a\right)$$
40	38 39	spcev	$$⊢\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a\to \exists ff:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a$$
41	37 40	syl	$$⊢\left(\neg x=y\wedge \left(x\in a\wedge y\in a\right)\right)\to \exists ff:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a$$
42		vex	$$⊢a\in \mathrm{V}$$
43	42	brdom	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\preccurlyeq a\leftrightarrow \exists ff:\left\{\varnothing ,1_{𝑜}\right\}\underset{1-1}{⟶}a$$
44	41 43	sylibr	$$⊢\left(\neg x=y\wedge \left(x\in a\wedge y\in a\right)\right)\to \left\{\varnothing ,1_{𝑜}\right\}\preccurlyeq a$$
45	44	expcom	$$⊢\left(x\in a\wedge y\in a\right)\to \left(\neg x=y\to \left\{\varnothing ,1_{𝑜}\right\}\preccurlyeq a\right)$$
46	45	rexlimivv	$$⊢\exists x\in a\exists y\in a\neg x=y\to \left\{\varnothing ,1_{𝑜}\right\}\preccurlyeq a$$
47	10 46	eqbrtrid	$$⊢\exists x\in a\exists y\in a\neg x=y\to 2_{𝑜}\preccurlyeq a$$
48	9 47	impbii	$$⊢2_{𝑜}\preccurlyeq a\leftrightarrow \exists x\in a\exists y\in a\neg x=y$$
49	6 8 48	3bitr2i	$$⊢1_{𝑜}\prec a\leftrightarrow \exists x\in a\exists y\in a\neg x=y$$
50	1 3 49	vtoclbg	$$⊢A\in V\to \left(1_{𝑜}\prec A\leftrightarrow \exists x\in A\exists y\in A\neg x=y\right)$$