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

Metamath Proof Explorer

Theorem offvalfv

Description: The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019)

Ref Expression
Hypotheses offvalfv.a 
|- ( ph -> A e. V )
offvalfv.f 
|- ( ph -> F Fn A )
offvalfv.g 
|- ( ph -> G Fn A )
Assertion offvalfv 
|- ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 offvalfv.a 
 |-  ( ph -> A e. V )
2 offvalfv.f 
 |-  ( ph -> F Fn A )
3 offvalfv.g 
 |-  ( ph -> G Fn A )
4 fnfvelrn 
 |-  ( ( F Fn A /\ x e. A ) -> ( F ` x ) e. ran F )
5 2 4 sylan 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. ran F )
6 fnfvelrn 
 |-  ( ( G Fn A /\ x e. A ) -> ( G ` x ) e. ran G )
7 3 6 sylan 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. ran G )
8 dffn5 
 |-  ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
9 2 8 sylib 
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
10 dffn5 
 |-  ( G Fn A <-> G = ( x e. A |-> ( G ` x ) ) )
11 3 10 sylib 
 |-  ( ph -> G = ( x e. A |-> ( G ` x ) ) )
12 1 5 7 9 11 offval2 
 |-  ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )