Metamath Proof Explorer


Theorem fovrnda

Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypothesis fovrnd.1 ( 𝜑𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
Assertion fovrnda ( ( 𝜑 ∧ ( 𝐴𝑅𝐵𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 fovrnd.1 ( 𝜑𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
2 fovrn ( ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶𝐴𝑅𝐵𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )
3 1 2 syl3an1 ( ( 𝜑𝐴𝑅𝐵𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )
4 3 3expb ( ( 𝜑 ∧ ( 𝐴𝑅𝐵𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )