Theorem 1sdom2

Description: Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un , see 1sdom2ALT . (Contributed by NM, 4-Apr-2007) Avoid ax-un . (Revised by BTernaryTau, 8-Dec-2024)

	Ref	Expression
Assertion	1sdom2	$$⊢1_{𝑜}\prec 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		2on0	$$⊢2_{𝑜}\ne \varnothing$$
2		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
3	2	0sdom	$$⊢\varnothing \prec 2_{𝑜}\leftrightarrow 2_{𝑜}\ne \varnothing$$
4	1 3	mpbir	$$⊢\varnothing \prec 2_{𝑜}$$
5		0sdom1dom	$$⊢\varnothing \prec 2_{𝑜}\leftrightarrow 1_{𝑜}\preccurlyeq 2_{𝑜}$$
6	4 5	mpbi	$$⊢1_{𝑜}\preccurlyeq 2_{𝑜}$$
7		snnen2o	$$⊢\neg \left\{\varnothing \right\}\approx 2_{𝑜}$$
8		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
9	8	breq1i	$$⊢1_{𝑜}\approx 2_{𝑜}\leftrightarrow \left\{\varnothing \right\}\approx 2_{𝑜}$$
10	7 9	mtbir	$$⊢\neg 1_{𝑜}\approx 2_{𝑜}$$
11		brsdom	$$⊢1_{𝑜}\prec 2_{𝑜}\leftrightarrow \left(1_{𝑜}\preccurlyeq 2_{𝑜}\wedge \neg 1_{𝑜}\approx 2_{𝑜}\right)$$
12	6 10 11	mpbir2an	$$⊢1_{𝑜}\prec 2_{𝑜}$$