Metamath Proof Explorer


Theorem ovmpoelrn

Description: An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020)

Ref Expression
Hypothesis ovmpoelrn.o 𝑂 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
Assertion ovmpoelrn ( ( ∀ 𝑥𝐴𝑦𝐵 𝐶𝑀𝑋𝐴𝑌𝐵 ) → ( 𝑋 𝑂 𝑌 ) ∈ 𝑀 )

Proof

Step Hyp Ref Expression
1 ovmpoelrn.o 𝑂 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
2 1 fmpo ( ∀ 𝑥𝐴𝑦𝐵 𝐶𝑀𝑂 : ( 𝐴 × 𝐵 ) ⟶ 𝑀 )
3 fovrn ( ( 𝑂 : ( 𝐴 × 𝐵 ) ⟶ 𝑀𝑋𝐴𝑌𝐵 ) → ( 𝑋 𝑂 𝑌 ) ∈ 𝑀 )
4 2 3 syl3an1b ( ( ∀ 𝑥𝐴𝑦𝐵 𝐶𝑀𝑋𝐴𝑌𝐵 ) → ( 𝑋 𝑂 𝑌 ) ∈ 𝑀 )