Description: An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ovmpoelrn.o | ⊢ 𝑂 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) | |
Assertion | ovmpoelrn | ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) ∈ 𝑀 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovmpoelrn.o | ⊢ 𝑂 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) | |
2 | 1 | fmpo | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ↔ 𝑂 : ( 𝐴 × 𝐵 ) ⟶ 𝑀 ) |
3 | fovrn | ⊢ ( ( 𝑂 : ( 𝐴 × 𝐵 ) ⟶ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) ∈ 𝑀 ) | |
4 | 2 3 | syl3an1b | ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) ∈ 𝑀 ) |