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

Metamath Proof Explorer

Theorem offn

Description: The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses offval.1 
|- ( ph -> F Fn A )
offval.2 
|- ( ph -> G Fn B )
offval.3 
|- ( ph -> A e. V )
offval.4 
|- ( ph -> B e. W )
offval.5 
|- ( A i^i B ) = S
Assertion offn 
|- ( ph -> ( F oF R G ) Fn S )

Proof

Step Hyp Ref Expression
1 offval.1 
 |-  ( ph -> F Fn A )
2 offval.2 
 |-  ( ph -> G Fn B )
3 offval.3 
 |-  ( ph -> A e. V )
4 offval.4 
 |-  ( ph -> B e. W )
5 offval.5 
 |-  ( A i^i B ) = S
6 ovex 
 |-  ( ( F ` x ) R ( G ` x ) ) e. _V
7 eqid 
 |-  ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) = ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) )
8 6 7 fnmpti 
 |-  ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) Fn S
9 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
10 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( G ` x ) = ( G ` x ) )
11 1 2 3 4 5 9 10 offval 
 |-  ( ph -> ( F oF R G ) = ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) )
12 11 fneq1d 
 |-  ( ph -> ( ( F oF R G ) Fn S <-> ( x e. S |-> ( ( F ` x ) R ( G ` x ) ) ) Fn S ) )
13 8 12 mpbiri 
 |-  ( ph -> ( F oF R G ) Fn S )