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

Metamath Proof Explorer

Theorem 0domg

Description: Any set dominates the empty set. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

Ref Expression
Assertion 0domg ⊢ A ∈ V → ∅ ≼ A

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 f1eq1 ⊢ f = ∅ → f : ∅ ⟶ 1-1 A ↔ ∅ : ∅ ⟶ 1-1 A
3 f10 ⊢ ∅ : ∅ ⟶ 1-1 A
4 1 2 3 ceqsexv2d ⊢ ∃ f f : ∅ ⟶ 1-1 A
5 brdom2g ⊢ ∅ ∈ V ∧ A ∈ V → ∅ ≼ A ↔ ∃ f f : ∅ ⟶ 1-1 A
6 1 5 mpan ⊢ A ∈ V → ∅ ≼ A ↔ ∃ f f : ∅ ⟶ 1-1 A
7 4 6 mpbiri ⊢ A ∈ V → ∅ ≼ A