Theorem ofcfval3

Description: General value of ( F oFC R C ) with no assumptions on functionality of F . (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Assertion	ofcfval3	|- ( ( F e. V /\ C e. W ) -> ( F oFC R C ) = ( x e. dom F |-> ( ( F ` x ) R C ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( F e. V -> F e. _V )
2	1	adantr	|- ( ( F e. V /\ C e. W ) -> F e. _V )
3		elex	|- ( C e. W -> C e. _V )
4	3	adantl	|- ( ( F e. V /\ C e. W ) -> C e. _V )
5		dmexg	|- ( F e. V -> dom F e. _V )
6		mptexg	|- ( dom F e. _V -> ( x e. dom F |-> ( ( F ` x ) R C ) ) e. _V )
7	5 6	syl	|- ( F e. V -> ( x e. dom F |-> ( ( F ` x ) R C ) ) e. _V )
8	7	adantr	|- ( ( F e. V /\ C e. W ) -> ( x e. dom F |-> ( ( F ` x ) R C ) ) e. _V )
9		simpl	|- ( ( f = F /\ c = C ) -> f = F )
10	9	dmeqd	|- ( ( f = F /\ c = C ) -> dom f = dom F )
11	9	fveq1d	|- ( ( f = F /\ c = C ) -> ( f ` x ) = ( F ` x ) )
12		simpr	|- ( ( f = F /\ c = C ) -> c = C )
13	11 12	oveq12d	|- ( ( f = F /\ c = C ) -> ( ( f ` x ) R c ) = ( ( F ` x ) R C ) )
14	10 13	mpteq12dv	|- ( ( f = F /\ c = C ) -> ( x e. dom f |-> ( ( f ` x ) R c ) ) = ( x e. dom F |-> ( ( F ` x ) R C ) ) )
15		df-ofc	|- oFC R = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) )
16	14 15	ovmpoga	|- ( ( F e. _V /\ C e. _V /\ ( x e. dom F |-> ( ( F ` x ) R C ) ) e. _V ) -> ( F oFC R C ) = ( x e. dom F |-> ( ( F ` x ) R C ) ) )
17	2 4 8 16	syl3anc	|- ( ( F e. V /\ C e. W ) -> ( F oFC R C ) = ( x e. dom F |-> ( ( F ` x ) R C ) ) )