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