Theorem faovcl

Description: Closure law for an operation, analogous to fovcl . (Contributed by Alexander van der Vekens, 26-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		faovcl.1	⊢ 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶
2		ffnaov	⊢ ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝑅 × 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) )
3	2	simprbi	⊢ ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 )
4	1 3	ax-mp	⊢ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶
5		eqidd	⊢ ( 𝑥 = 𝐴 → 𝐹 = 𝐹 )
6		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
7		eqidd	⊢ ( 𝑥 = 𝐴 → 𝑦 = 𝑦 )
8	5 6 7	aoveq123d	⊢ ( 𝑥 = 𝐴 → (( 𝑥 𝐹 𝑦 )) = (( 𝐴 𝐹 𝑦 )) )
9	8	eleq1d	⊢ ( 𝑥 = 𝐴 → ( (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ↔ (( 𝐴 𝐹 𝑦 )) ∈ 𝐶 ) )
10		eqidd	⊢ ( 𝑦 = 𝐵 → 𝐹 = 𝐹 )
11		eqidd	⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐴 )
12		id	⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
13	10 11 12	aoveq123d	⊢ ( 𝑦 = 𝐵 → (( 𝐴 𝐹 𝑦 )) = (( 𝐴 𝐹 𝐵 )) )
14	13	eleq1d	⊢ ( 𝑦 = 𝐵 → ( (( 𝐴 𝐹 𝑦 )) ∈ 𝐶 ↔ (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 ) )
15	9 14	rspc2v	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 → (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 ) )
16	4 15	mpi	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 )