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

Proof

Step	Hyp	Ref	Expression
1		fovcld.1	|- ( ph -> F : ( R X. S ) --> C )
2		3simpc	|- ( ( ph /\ A e. R /\ B e. S ) -> ( A e. R /\ B e. S ) )
3		ffnov	|- ( F : ( R X. S ) --> C <-> ( F Fn ( R X. S ) /\ A. x e. R A. y e. S ( x F y ) e. C ) )
4	3	simprbi	|- ( F : ( R X. S ) --> C -> A. x e. R A. y e. S ( x F y ) e. C )
5	1 4	syl	|- ( ph -> A. x e. R A. y e. S ( x F y ) e. C )
6	5	3ad2ant1	|- ( ( ph /\ A e. R /\ B e. S ) -> A. x e. R A. y e. S ( x F y ) e. C )
7		oveq1	|- ( x = A -> ( x F y ) = ( A F y ) )
8	7	eleq1d	|- ( x = A -> ( ( x F y ) e. C <-> ( A F y ) e. C ) )
9		oveq2	|- ( y = B -> ( A F y ) = ( A F B ) )
10	9	eleq1d	|- ( y = B -> ( ( A F y ) e. C <-> ( A F B ) e. C ) )
11	8 10	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 ) )
12	2 6 11	sylc	|- ( ( ph /\ A e. R /\ B e. S ) -> ( A F B ) e. C )