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	$$⊢F:R\times S⟶C$$
Assertion	faovcl	$$⊢\left(A\in R\wedge B\in S\right)\to ((AFB))\in C$$

Proof

Step	Hyp	Ref	Expression
1		faovcl.1	$$⊢F:R\times S⟶C$$
2		ffnaov	$$⊢F:R\times S⟶C\leftrightarrow \left(FFn\left(R\times S\right)\wedge \forall x\in R\forall y\in S((xFy))\in C\right)$$
3	2	simprbi	$$⊢F:R\times S⟶C\to \forall x\in R\forall y\in S((xFy))\in C$$
4	1 3	ax-mp	$$⊢\forall x\in R\forall y\in S((xFy))\in C$$
5		eqidd	$$⊢x=A\to F=F$$
6		id	$$⊢x=A\to x=A$$
7		eqidd	$$⊢x=A\to y=y$$
8	5 6 7	aoveq123d	$$⊢x=A\to ((xFy))=((AFy))$$
9	8	eleq1d	$$⊢x=A\to \left(((xFy))\in C\leftrightarrow ((AFy))\in C\right)$$
10		eqidd	$$⊢y=B\to F=F$$
11		eqidd	$$⊢y=B\to A=A$$
12		id	$$⊢y=B\to y=B$$
13	10 11 12	aoveq123d	$$⊢y=B\to ((AFy))=((AFB))$$
14	13	eleq1d	$$⊢y=B\to \left(((AFy))\in C\leftrightarrow ((AFB))\in C\right)$$
15	9 14	rspc2v	$$⊢\left(A\in R\wedge B\in S\right)\to \left(\forall x\in R\forall y\in S((xFy))\in C\to ((AFB))\in C\right)$$
16	4 15	mpi	$$⊢\left(A\in R\wedge B\in S\right)\to ((AFB))\in C$$