snnen2o

Description: A singleton { A } is never equinumerous with the ordinal number 2. This holds for proper singletons ( A e.V ) as well as for singletons being the empty set ( A e/ V ). (Contributed by AV, 6-Aug-2019) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 1-Dec-2024)

		Ref	Expression
	Assertion	snnen2o	$⊢ \neg \{A\} \approx 2_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
2		0ex	$⊢ \emptyset \in V$
3		1oex	$⊢ 1_{𝑜} \in V$
4		1n0	$⊢ 1_{𝑜} \neq \emptyset$
5	4	necomi	$⊢ \emptyset \neq 1_{𝑜}$
6		prnesn	$⊢ (\emptyset \in V \land 1_{𝑜} \in V \land \emptyset \neq 1_{𝑜}) \to \{\emptyset, 1_{𝑜}\} \neq \{x\}$
7	2 3 5 6	mp3an	$⊢ \{\emptyset, 1_{𝑜}\} \neq \{x\}$
8	1 7	eqnetri	$⊢ 2_{𝑜} \neq \{x\}$
9	8	neii	$⊢ \neg 2_{𝑜} = \{x\}$
10	9	nex	$⊢ \neg \exists x 2_{𝑜} = \{x\}$
11		2on0	$⊢ 2_{𝑜} \neq \emptyset$
12		f1cdmsn	$⊢ (f^{-1} : 2_{𝑜} \underset{1-1}{⟶} \{A\} \land 2_{𝑜} \neq \emptyset) \to \exists x 2_{𝑜} = \{x\}$
13	11 12	mpan2	$⊢ f^{-1} : 2_{𝑜} \underset{1-1}{⟶} \{A\} \to \exists x 2_{𝑜} = \{x\}$
14	10 13	mto	$⊢ \neg f^{-1} : 2_{𝑜} \underset{1-1}{⟶} \{A\}$
15		f1ocnv	$⊢ f : \{A\} \underset{1-1 onto}{⟶} 2_{𝑜} \to f^{-1} : 2_{𝑜} \underset{1-1 onto}{⟶} \{A\}$
16		f1of1	$⊢ f^{-1} : 2_{𝑜} \underset{1-1 onto}{⟶} \{A\} \to f^{-1} : 2_{𝑜} \underset{1-1}{⟶} \{A\}$
17	15 16	syl	$⊢ f : \{A\} \underset{1-1 onto}{⟶} 2_{𝑜} \to f^{-1} : 2_{𝑜} \underset{1-1}{⟶} \{A\}$
18	14 17	mto	$⊢ \neg f : \{A\} \underset{1-1 onto}{⟶} 2_{𝑜}$
19	18	nex	$⊢ \neg \exists f f : \{A\} \underset{1-1 onto}{⟶} 2_{𝑜}$
20		snex	$⊢ \{A\} \in V$
21		2oex	$⊢ 2_{𝑜} \in V$
22		breng	$⊢ (\{A\} \in V \land 2_{𝑜} \in V) \to (\{A\} \approx 2_{𝑜} \leftrightarrow \exists f f : \{A\} \underset{1-1 onto}{⟶} 2_{𝑜})$
23	20 21 22	mp2an	$⊢ \{A\} \approx 2_{𝑜} \leftrightarrow \exists f f : \{A\} \underset{1-1 onto}{⟶} 2_{𝑜}$
24	19 23	mtbir	$⊢ \neg \{A\} \approx 2_{𝑜}$

Metamath Proof Explorer

Theorem snnen2o

Proof