Theorem 0wdom

Description: Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	0wdom	⊢ ( 𝑋 ∈ 𝑉 → ∅ ≼* 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∅ = ∅
2	1	orci	⊢ ( ∅ = ∅ ∨ ∃ 𝑧 𝑧 : 𝑋 –onto→ ∅ )
3		brwdom	⊢ ( 𝑋 ∈ 𝑉 → ( ∅ ≼* 𝑋 ↔ ( ∅ = ∅ ∨ ∃ 𝑧 𝑧 : 𝑋 –onto→ ∅ ) ) )
4	2 3	mpbiri	⊢ ( 𝑋 ∈ 𝑉 → ∅ ≼* 𝑋 )