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 X. S ) --> C
Assertion	faovcl	|- ( ( A e. R /\ B e. S ) -> (( A F B )) e. C )

Proof

Step	Hyp	Ref	Expression
1		faovcl.1	|- F : ( R X. S ) --> C
2		ffnaov	|- ( F : ( R X. S ) --> C <-> ( F Fn ( R X. S ) /\ A. x e. R A. y e. S (( x F y )) e. C ) )
3	2	simprbi	|- ( F : ( R X. S ) --> C -> A. x e. R A. y e. S (( x F y )) e. C )
4	1 3	ax-mp	|- A. x e. R A. y e. S (( x F y )) e. C
5		eqidd	|- ( x = A -> F = F )
6		id	|- ( x = A -> x = A )
7		eqidd	|- ( x = A -> y = y )
8	5 6 7	aoveq123d	|- ( x = A -> (( x F y )) = (( A F y )) )
9	8	eleq1d	|- ( x = A -> ( (( x F y )) e. C <-> (( A F y )) e. C ) )
10		eqidd	|- ( y = B -> F = F )
11		eqidd	|- ( y = B -> A = A )
12		id	|- ( y = B -> y = B )
13	10 11 12	aoveq123d	|- ( y = B -> (( A F y )) = (( A F B )) )
14	13	eleq1d	|- ( y = B -> ( (( A F y )) e. C <-> (( A F B )) e. C ) )
15	9 14	rspc2v	|- ( ( A e. R /\ B e. S ) -> ( A. x e. R A. y e. S (( x F y )) e. C -> (( A F B )) e. C ) )
16	4 15	mpi	|- ( ( A e. R /\ B e. S ) -> (( A F B )) e. C )