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 )