Theorem oprres

Description: The restriction of an operation is an operation. (Contributed by NM, 1-Feb-2008) (Revised by AV, 19-Oct-2021)

	Ref	Expression
Hypotheses	oprres.v	|- ( ( ph /\ x e. Y /\ y e. Y ) -> ( x F y ) = ( x G y ) )
	oprres.s	|- ( ph -> Y C_ X )
	oprres.f	|- ( ph -> F : ( Y X. Y ) --> R )
	oprres.g	|- ( ph -> G : ( X X. X ) --> S )
Assertion	oprres	|- ( ph -> F = ( G |` ( Y X. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		oprres.v	|- ( ( ph /\ x e. Y /\ y e. Y ) -> ( x F y ) = ( x G y ) )
2		oprres.s	|- ( ph -> Y C_ X )
3		oprres.f	|- ( ph -> F : ( Y X. Y ) --> R )
4		oprres.g	|- ( ph -> G : ( X X. X ) --> S )
5	1	3expb	|- ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( x F y ) = ( x G y ) )
6		ovres	|- ( ( x e. Y /\ y e. Y ) -> ( x ( G |` ( Y X. Y ) ) y ) = ( x G y ) )
7	6	adantl	|- ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( x ( G |` ( Y X. Y ) ) y ) = ( x G y ) )
8	5 7	eqtr4d	|- ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) )
9	8	ralrimivva	|- ( ph -> A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) )
10		eqid	|- ( Y X. Y ) = ( Y X. Y )
11	9 10	jctil	|- ( ph -> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) )
12	3	ffnd	|- ( ph -> F Fn ( Y X. Y ) )
13	4	ffnd	|- ( ph -> G Fn ( X X. X ) )
14		xpss12	|- ( ( Y C_ X /\ Y C_ X ) -> ( Y X. Y ) C_ ( X X. X ) )
15	2 2 14	syl2anc	|- ( ph -> ( Y X. Y ) C_ ( X X. X ) )
16		fnssres	|- ( ( G Fn ( X X. X ) /\ ( Y X. Y ) C_ ( X X. X ) ) -> ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) )
17	13 15 16	syl2anc	|- ( ph -> ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) )
18		eqfnov	|- ( ( F Fn ( Y X. Y ) /\ ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) ) -> ( F = ( G |` ( Y X. Y ) ) <-> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) ) )
19	12 17 18	syl2anc	|- ( ph -> ( F = ( G |` ( Y X. Y ) ) <-> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) ) )
20	11 19	mpbird	|- ( ph -> F = ( G |` ( Y X. Y ) ) )