Theorem brwdom3i

Description: Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015)

	Ref	Expression
Assertion	brwdom3i	⊢ ( 𝑋 ≼* 𝑌 → ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		relwdom	⊢ Rel ≼*
2	1	brrelex1i	⊢ ( 𝑋 ≼* 𝑌 → 𝑋 ∈ V )
3	1	brrelex2i	⊢ ( 𝑋 ≼* 𝑌 → 𝑌 ∈ V )
4		brwdom3	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
5	2 3 4	syl2anc	⊢ ( 𝑋 ≼* 𝑌 → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
6	5	ibi	⊢ ( 𝑋 ≼* 𝑌 → ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) )