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 ( 𝐴𝑉 → ∅ ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 0ex ∅ ∈ V
2 f1eq1 ( 𝑓 = ∅ → ( 𝑓 : ∅ –1-1𝐴 ↔ ∅ : ∅ –1-1𝐴 ) )
3 f10 ∅ : ∅ –1-1𝐴
4 1 2 3 ceqsexv2d 𝑓 𝑓 : ∅ –1-1𝐴
5 brdom2g ( ( ∅ ∈ V ∧ 𝐴𝑉 ) → ( ∅ ≼ 𝐴 ↔ ∃ 𝑓 𝑓 : ∅ –1-1𝐴 ) )
6 1 5 mpan ( 𝐴𝑉 → ( ∅ ≼ 𝐴 ↔ ∃ 𝑓 𝑓 : ∅ –1-1𝐴 ) )
7 4 6 mpbiri ( 𝐴𝑉 → ∅ ≼ 𝐴 )