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

Metamath Proof Explorer

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 (1_{𝑜} ≺ A \leftrightarrow \exists x \in A \exists y \in A \neg x = y)$

Proof

Step	Hyp	Ref	Expression
1		1sdom2dom	$⊢ 1_{𝑜} ≺ A \leftrightarrow 2_{𝑜} ≼ A$
2		2dom	$⊢ 2_{𝑜} ≼ A \to \exists x \in A \exists y \in A \neg x = y$
3		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
4	3	2rexbii	$⊢ \exists x \in A \exists y \in A x \neq y \leftrightarrow \exists x \in A \exists y \in A \neg x = y$
5		rex2dom	$⊢ (A \in V \land \exists x \in A \exists y \in A x \neq y) \to 2_{𝑜} ≼ A$
6	4 5	sylan2br	$⊢ (A \in V \land \exists x \in A \exists y \in A \neg x = y) \to 2_{𝑜} ≼ A$
7	6	ex	$⊢ A \in V \to (\exists x \in A \exists y \in A \neg x = y \to 2_{𝑜} ≼ A)$
8	2 7	impbid2	$⊢ A \in V \to (2_{𝑜} ≼ A \leftrightarrow \exists x \in A \exists y \in A \neg x = y)$
9	1 8	bitrid	$⊢ A \in V \to (1_{𝑜} ≺ A \leftrightarrow \exists x \in A \exists y \in A \neg x = y)$