Theorem 2dom

Description: A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004)

	Ref	Expression
Assertion	2dom	$$⊢2_{𝑜}\preccurlyeq A\to \exists x\in A\exists y\in A\neg x=y$$

Proof

Step	Hyp	Ref	Expression
1		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
2	1	breq1i	$$⊢2_{𝑜}\preccurlyeq A\leftrightarrow \left\{\varnothing ,\left\{\varnothing \right\}\right\}\preccurlyeq A$$
3		brdomi	$$⊢\left\{\varnothing ,\left\{\varnothing \right\}\right\}\preccurlyeq A\to \exists ff:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A$$
4	2 3	sylbi	$$⊢2_{𝑜}\preccurlyeq A\to \exists ff:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A$$
5		f1f	$$⊢f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\to f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}⟶A$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	6	prid1	$$⊢\varnothing \in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
8		ffvelrn	$$⊢\left(f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}⟶A\wedge \varnothing \in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)\to f\left(\varnothing \right)\in A$$
9	5 7 8	sylancl	$$⊢f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\to f\left(\varnothing \right)\in A$$
10		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
11	10	prid2	$$⊢\left\{\varnothing \right\}\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
12		ffvelrn	$$⊢\left(f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}⟶A\wedge \left\{\varnothing \right\}\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)\to f\left(\left\{\varnothing \right\}\right)\in A$$
13	5 11 12	sylancl	$$⊢f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\to f\left(\left\{\varnothing \right\}\right)\in A$$
14		0nep0	$$⊢\varnothing \ne \left\{\varnothing \right\}$$
15	14	neii	$$⊢\neg \varnothing =\left\{\varnothing \right\}$$
16		f1fveq	$$⊢\left(f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\wedge \left(\varnothing \in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\wedge \left\{\varnothing \right\}\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)\right)\to \left(f\left(\varnothing \right)=f\left(\left\{\varnothing \right\}\right)\leftrightarrow \varnothing =\left\{\varnothing \right\}\right)$$
17	7 11 16	mpanr12	$$⊢f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\to \left(f\left(\varnothing \right)=f\left(\left\{\varnothing \right\}\right)\leftrightarrow \varnothing =\left\{\varnothing \right\}\right)$$
18	15 17	mtbiri	$$⊢f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\to \neg f\left(\varnothing \right)=f\left(\left\{\varnothing \right\}\right)$$
19		eqeq1	$$⊢x=f\left(\varnothing \right)\to \left(x=y\leftrightarrow f\left(\varnothing \right)=y\right)$$
20	19	notbid	$$⊢x=f\left(\varnothing \right)\to \left(\neg x=y\leftrightarrow \neg f\left(\varnothing \right)=y\right)$$
21		eqeq2	$$⊢y=f\left(\left\{\varnothing \right\}\right)\to \left(f\left(\varnothing \right)=y\leftrightarrow f\left(\varnothing \right)=f\left(\left\{\varnothing \right\}\right)\right)$$
22	21	notbid	$$⊢y=f\left(\left\{\varnothing \right\}\right)\to \left(\neg f\left(\varnothing \right)=y\leftrightarrow \neg f\left(\varnothing \right)=f\left(\left\{\varnothing \right\}\right)\right)$$
23	20 22	rspc2ev	$$⊢\left(f\left(\varnothing \right)\in A\wedge f\left(\left\{\varnothing \right\}\right)\in A\wedge \neg f\left(\varnothing \right)=f\left(\left\{\varnothing \right\}\right)\right)\to \exists x\in A\exists y\in A\neg x=y$$
24	9 13 18 23	syl3anc	$$⊢f:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\to \exists x\in A\exists y\in A\neg x=y$$
25	24	exlimiv	$$⊢\exists ff:\left\{\varnothing ,\left\{\varnothing \right\}\right\}\underset{1-1}{⟶}A\to \exists x\in A\exists y\in A\neg x=y$$
26	4 25	syl	$$⊢2_{𝑜}\preccurlyeq A\to \exists x\in A\exists y\in A\neg x=y$$