Theorem elrnmpoid

Description: Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	elrnmpoid.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	elrnmpoid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑦 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		elrnmpoid.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2	1	fnmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
3	2	3ad2ant3	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ) → 𝐹 Fn ( 𝐴 × 𝐵 ) )
4		simp1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ) → 𝑥 ∈ 𝐴 )
5		simp2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ) → 𝑦 ∈ 𝐵 )
6		fnovrn	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 𝐹 𝑦 ) ∈ ran 𝐹 )
7	3 4 5 6	syl3anc	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑦 ) ∈ ran 𝐹 )