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

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