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

Metamath Proof Explorer

Theorem dom0

Description: A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

		Ref	Expression
	Assertion	dom0	$⊢ A ≼ \emptyset \leftrightarrow A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		brdomi	$⊢ A ≼ \emptyset \to \exists f f : A \underset{1-1}{⟶} \emptyset$
2		f1f	$⊢ f : A \underset{1-1}{⟶} \emptyset \to f : A ⟶ \emptyset$
3		f00	$⊢ f : A ⟶ \emptyset \leftrightarrow (f = \emptyset \land A = \emptyset)$
4	3	simprbi	$⊢ f : A ⟶ \emptyset \to A = \emptyset$
5	2 4	syl	$⊢ f : A \underset{1-1}{⟶} \emptyset \to A = \emptyset$
6	5	exlimiv	$⊢ \exists f f : A \underset{1-1}{⟶} \emptyset \to A = \emptyset$
7	1 6	syl	$⊢ A ≼ \emptyset \to A = \emptyset$
8		en0	$⊢ A \approx \emptyset \leftrightarrow A = \emptyset$
9		endom	$⊢ A \approx \emptyset \to A ≼ \emptyset$
10	8 9	sylbir	$⊢ A = \emptyset \to A ≼ \emptyset$
11	7 10	impbii	$⊢ A ≼ \emptyset \leftrightarrow A = \emptyset$