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	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) ∈ 𝑀 )