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

Metamath Proof Explorer

Theorem sdom0

Description: The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

		Ref	Expression
	Assertion	sdom0	$⊢ \neg A ≺ \emptyset$

Proof

Step	Hyp	Ref	Expression
1		dom0	$⊢ A ≼ \emptyset \leftrightarrow A = \emptyset$
2		en0	$⊢ A \approx \emptyset \leftrightarrow A = \emptyset$
3	1 2	sylbb2	$⊢ A ≼ \emptyset \to A \approx \emptyset$
4		iman	$⊢ (A ≼ \emptyset \to A \approx \emptyset) \leftrightarrow \neg (A ≼ \emptyset \land \neg A \approx \emptyset)$
5	3 4	mpbi	$⊢ \neg (A ≼ \emptyset \land \neg A \approx \emptyset)$
6		brsdom	$⊢ A ≺ \emptyset \leftrightarrow (A ≼ \emptyset \land \neg A \approx \emptyset)$
7	5 6	mtbir	$⊢ \neg A ≺ \emptyset$