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	⊢ ¬ 𝐴 ≺ ∅

Proof

Step	Hyp	Ref	Expression
1		dom0	⊢ ( 𝐴 ≼ ∅ ↔ 𝐴 = ∅ )
2		en0	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
3	1 2	sylbb2	⊢ ( 𝐴 ≼ ∅ → 𝐴 ≈ ∅ )
4		iman	⊢ ( ( 𝐴 ≼ ∅ → 𝐴 ≈ ∅ ) ↔ ¬ ( 𝐴 ≼ ∅ ∧ ¬ 𝐴 ≈ ∅ ) )
5	3 4	mpbi	⊢ ¬ ( 𝐴 ≼ ∅ ∧ ¬ 𝐴 ≈ ∅ )
6		brsdom	⊢ ( 𝐴 ≺ ∅ ↔ ( 𝐴 ≼ ∅ ∧ ¬ 𝐴 ≈ ∅ ) )
7	5 6	mtbir	⊢ ¬ 𝐴 ≺ ∅