Metamath Proof Explorer


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 ( 𝑋* 𝑌 → ∃ 𝑓𝑥𝑋𝑦𝑌 𝑥 = ( 𝑓𝑦 ) )