This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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_{𝑜} ≺ 2_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		2on0	$⊢ 2_{𝑜} \neq \emptyset$
2		2oex	$⊢ 2_{𝑜} \in V$
3	2	0sdom	$⊢ \emptyset ≺ 2_{𝑜} \leftrightarrow 2_{𝑜} \neq \emptyset$
4	1 3	mpbir	$⊢ \emptyset ≺ 2_{𝑜}$
5		0sdom1dom	$⊢ \emptyset ≺ 2_{𝑜} \leftrightarrow 1_{𝑜} ≼ 2_{𝑜}$
6	4 5	mpbi	$⊢ 1_{𝑜} ≼ 2_{𝑜}$
7		snnen2o	$⊢ \neg \{\emptyset\} \approx 2_{𝑜}$
8		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
9	8	breq1i	$⊢ 1_{𝑜} \approx 2_{𝑜} \leftrightarrow \{\emptyset\} \approx 2_{𝑜}$
10	7 9	mtbir	$⊢ \neg 1_{𝑜} \approx 2_{𝑜}$
11		brsdom	$⊢ 1_{𝑜} ≺ 2_{𝑜} \leftrightarrow (1_{𝑜} ≼ 2_{𝑜} \land \neg 1_{𝑜} \approx 2_{𝑜})$
12	6 10 11	mpbir2an	$⊢ 1_{𝑜} ≺ 2_{𝑜}$