Theorem fovcld

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007) (Revised by Thierry Arnoux, 17-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		fovcld.1	⊢ ( 𝜑 → 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
2		3simpc	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) )
3		ffnov	⊢ ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝑅 × 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )
4	3	simprbi	⊢ ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 )
5	1 4	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 )
6	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 )
7		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ) = ( 𝐴 𝐹 𝑦 ) )
8	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ↔ ( 𝐴 𝐹 𝑦 ) ∈ 𝐶 ) )
9		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦 ) = ( 𝐴 𝐹 𝐵 ) )
10	9	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐹 𝑦 ) ∈ 𝐶 ↔ ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 ) )
11	8 10	rspc2v	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 ) )
12	2 6 11	sylc	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )