Theorem fovcl

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007)

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

Proof

Step	Hyp	Ref	Expression
1		fovcl.1	⊢ 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶
2		ffnov	⊢ ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝑅 × 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )
3	2	simprbi	⊢ ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 )
4	1 3	ax-mp	⊢ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶
5		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ) = ( 𝐴 𝐹 𝑦 ) )
6	5	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ↔ ( 𝐴 𝐹 𝑦 ) ∈ 𝐶 ) )
7		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦 ) = ( 𝐴 𝐹 𝐵 ) )
8	7	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐹 𝑦 ) ∈ 𝐶 ↔ ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 ) )
9	6 8	rspc2v	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 ) )
10	4 9	mpi	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )