rex2dom

Description: A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024)

		Ref	Expression
	Assertion	rex2dom	$⊢ (A \in V \land \exists x \in A \exists y \in A x \neq y) \to 2_{𝑜} ≼ A$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in V \to A \in V$
2		prssi	$⊢ (x \in A \land y \in A) \to \{x, y\} \subseteq A$
3		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
4		0ex	$⊢ \emptyset \in V$
5	4	a1i	$⊢ x \neq y \to \emptyset \in V$
6		1oex	$⊢ 1_{𝑜} \in V$
7	6	a1i	$⊢ x \neq y \to 1_{𝑜} \in V$
8		vex	$⊢ x \in V$
9	8	a1i	$⊢ x \neq y \to x \in V$
10		vex	$⊢ y \in V$
11	10	a1i	$⊢ x \neq y \to y \in V$
12		1n0	$⊢ 1_{𝑜} \neq \emptyset$
13	12	necomi	$⊢ \emptyset \neq 1_{𝑜}$
14	13	a1i	$⊢ x \neq y \to \emptyset \neq 1_{𝑜}$
15		id	$⊢ x \neq y \to x \neq y$
16	5 7 9 11 14 15	en2prd	$⊢ x \neq y \to \{\emptyset, 1_{𝑜}\} \approx \{x, y\}$
17	3 16	eqbrtrid	$⊢ x \neq y \to 2_{𝑜} \approx \{x, y\}$
18		endom	$⊢ 2_{𝑜} \approx \{x, y\} \to 2_{𝑜} ≼ \{x, y\}$
19	17 18	syl	$⊢ x \neq y \to 2_{𝑜} ≼ \{x, y\}$
20		domssr	$⊢ (A \in V \land \{x, y\} \subseteq A \land 2_{𝑜} ≼ \{x, y\}) \to 2_{𝑜} ≼ A$
21	20	3expib	$⊢ A \in V \to ((\{x, y\} \subseteq A \land 2_{𝑜} ≼ \{x, y\}) \to 2_{𝑜} ≼ A)$
22	2 19 21	syl2ani	$⊢ A \in V \to (((x \in A \land y \in A) \land x \neq y) \to 2_{𝑜} ≼ A)$
23	22	expd	$⊢ A \in V \to ((x \in A \land y \in A) \to (x \neq y \to 2_{𝑜} ≼ A))$
24	23	rexlimdvv	$⊢ A \in V \to (\exists x \in A \exists y \in A x \neq y \to 2_{𝑜} ≼ A)$
25	1 24	syl	$⊢ A \in V \to (\exists x \in A \exists y \in A x \neq y \to 2_{𝑜} ≼ A)$
26	25	imp	$⊢ (A \in V \land \exists x \in A \exists y \in A x \neq y) \to 2_{𝑜} ≼ A$

Metamath Proof Explorer