Theorem brwdomi

Description: Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	brwdomi	⊢ ( 𝑋 ≼* 𝑌 → ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		relwdom	⊢ Rel ≼*
2	1	brrelex2i	⊢ ( 𝑋 ≼* 𝑌 → 𝑌 ∈ V )
3		brwdom	⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
4	2 3	syl	⊢ ( 𝑋 ≼* 𝑌 → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
5	4	ibi	⊢ ( 𝑋 ≼* 𝑌 → ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )