Description: Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | brwdom3i | ⊢ ( 𝑋 ≼* 𝑌 → ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) |
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 | ⊢ ( 𝑋 ≼* 𝑌 → ∃ 𝑓 ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑥 = ( 𝑓 ‘ 𝑦 ) ) |