This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )