sdom1

Description: A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 12-Dec-2024)

		Ref	Expression
	Assertion	sdom1	$⊢ A ≺ 1_{𝑜} \leftrightarrow A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
2	1	breq2i	$⊢ A ≼ 1_{𝑜} \leftrightarrow A ≼ \{\emptyset\}$
3		brdomi	$⊢ A ≼ \{\emptyset\} \to \exists f f : A \underset{1-1}{⟶} \{\emptyset\}$
4		f1cdmsn	$⊢ (f : A \underset{1-1}{⟶} \{\emptyset\} \land A \neq \emptyset) \to \exists x A = \{x\}$
5		vex	$⊢ x \in V$
6	5	ensn1	$⊢ \{x\} \approx 1_{𝑜}$
7		breq1	$⊢ A = \{x\} \to (A \approx 1_{𝑜} \leftrightarrow \{x\} \approx 1_{𝑜})$
8	6 7	mpbiri	$⊢ A = \{x\} \to A \approx 1_{𝑜}$
9	8	exlimiv	$⊢ \exists x A = \{x\} \to A \approx 1_{𝑜}$
10	4 9	syl	$⊢ (f : A \underset{1-1}{⟶} \{\emptyset\} \land A \neq \emptyset) \to A \approx 1_{𝑜}$
11	10	expcom	$⊢ A \neq \emptyset \to (f : A \underset{1-1}{⟶} \{\emptyset\} \to A \approx 1_{𝑜})$
12	11	exlimdv	$⊢ A \neq \emptyset \to (\exists f f : A \underset{1-1}{⟶} \{\emptyset\} \to A \approx 1_{𝑜})$
13	3 12	syl5	$⊢ A \neq \emptyset \to (A ≼ \{\emptyset\} \to A \approx 1_{𝑜})$
14	2 13	biimtrid	$⊢ A \neq \emptyset \to (A ≼ 1_{𝑜} \to A \approx 1_{𝑜})$
15		iman	$⊢ (A ≼ 1_{𝑜} \to A \approx 1_{𝑜}) \leftrightarrow \neg (A ≼ 1_{𝑜} \land \neg A \approx 1_{𝑜})$
16	14 15	sylib	$⊢ A \neq \emptyset \to \neg (A ≼ 1_{𝑜} \land \neg A \approx 1_{𝑜})$
17		brsdom	$⊢ A ≺ 1_{𝑜} \leftrightarrow (A ≼ 1_{𝑜} \land \neg A \approx 1_{𝑜})$
18	16 17	sylnibr	$⊢ A \neq \emptyset \to \neg A ≺ 1_{𝑜}$
19	18	necon4ai	$⊢ A ≺ 1_{𝑜} \to A = \emptyset$
20		1n0	$⊢ 1_{𝑜} \neq \emptyset$
21		1oex	$⊢ 1_{𝑜} \in V$
22	21	0sdom	$⊢ \emptyset ≺ 1_{𝑜} \leftrightarrow 1_{𝑜} \neq \emptyset$
23	20 22	mpbir	$⊢ \emptyset ≺ 1_{𝑜}$
24		breq1	$⊢ A = \emptyset \to (A ≺ 1_{𝑜} \leftrightarrow \emptyset ≺ 1_{𝑜})$
25	23 24	mpbiri	$⊢ A = \emptyset \to A ≺ 1_{𝑜}$
26	19 25	impbii	$⊢ A ≺ 1_{𝑜} \leftrightarrow A = \emptyset$

Metamath Proof Explorer

Theorem sdom1

Proof