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) Avoid ax-un . (Revised by BTernaryTau, 30-Dec-2024)

	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		1sdom2dom	$$⊢1_{𝑜}\prec A\leftrightarrow 2_{𝑜}\preccurlyeq A$$
2		2dom	$$⊢2_{𝑜}\preccurlyeq A\to \exists x\in A\exists y\in A\neg x=y$$
3		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
4	3	2rexbii	$$⊢\exists x\in A\exists y\in Ax\ne y\leftrightarrow \exists x\in A\exists y\in A\neg x=y$$
5		rex2dom	$$⊢\left(A\in V\wedge \exists x\in A\exists y\in Ax\ne y\right)\to 2_{𝑜}\preccurlyeq A$$
6	4 5	sylan2br	$$⊢\left(A\in V\wedge \exists x\in A\exists y\in A\neg x=y\right)\to 2_{𝑜}\preccurlyeq A$$
7	6	ex	$$⊢A\in V\to \left(\exists x\in A\exists y\in A\neg x=y\to 2_{𝑜}\preccurlyeq A\right)$$
8	2 7	impbid2	$$⊢A\in V\to \left(2_{𝑜}\preccurlyeq A\leftrightarrow \exists x\in A\exists y\in A\neg x=y\right)$$
9	1 8	bitrid	$$⊢A\in V\to \left(1_{𝑜}\prec A\leftrightarrow \exists x\in A\exists y\in A\neg x=y\right)$$