Metamath Proof Explorer

Theorem offval2

Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses offval2.1 
|- ( ph -> A e. V )
offval2.2 
|- ( ( ph /\ x e. A ) -> B e. W )
offval2.3 
|- ( ( ph /\ x e. A ) -> C e. X )
offval2.4 
|- ( ph -> F = ( x e. A |-> B ) )
offval2.5 
|- ( ph -> G = ( x e. A |-> C ) )
Assertion offval2 
|- ( ph -> ( F oF R G ) = ( x e. A |-> ( B R C ) ) )

Proof

Step Hyp Ref Expression
1 offval2.1 
 |-  ( ph -> A e. V )
2 offval2.2 
 |-  ( ( ph /\ x e. A ) -> B e. W )
3 offval2.3 
 |-  ( ( ph /\ x e. A ) -> C e. X )
4 offval2.4 
 |-  ( ph -> F = ( x e. A |-> B ) )
5 offval2.5 
 |-  ( ph -> G = ( x e. A |-> C ) )
6 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. W )
7 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
8 7 fnmpt 
 |-  ( A. x e. A B e. W -> ( x e. A |-> B ) Fn A )
9 6 8 syl 
 |-  ( ph -> ( x e. A |-> B ) Fn A )
10 4 fneq1d 
 |-  ( ph -> ( F Fn A <-> ( x e. A |-> B ) Fn A ) )
11 9 10 mpbird 
 |-  ( ph -> F Fn A )
12 3 ralrimiva 
 |-  ( ph -> A. x e. A C e. X )
13 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
14 13 fnmpt 
 |-  ( A. x e. A C e. X -> ( x e. A |-> C ) Fn A )
15 12 14 syl 
 |-  ( ph -> ( x e. A |-> C ) Fn A )
16 5 fneq1d 
 |-  ( ph -> ( G Fn A <-> ( x e. A |-> C ) Fn A ) )
17 15 16 mpbird 
 |-  ( ph -> G Fn A )
18 inidm 
 |-  ( A i^i A ) = A
19 4 adantr 
 |-  ( ( ph /\ y e. A ) -> F = ( x e. A |-> B ) )
20 19 fveq1d 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) = ( ( x e. A |-> B ) ` y ) )
21 5 adantr 
 |-  ( ( ph /\ y e. A ) -> G = ( x e. A |-> C ) )
22 21 fveq1d 
 |-  ( ( ph /\ y e. A ) -> ( G ` y ) = ( ( x e. A |-> C ) ` y ) )
23 11 17 1 1 18 20 22 offval 
 |-  ( ph -> ( F oF R G ) = ( y e. A |-> ( ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y ) ) ) )
24 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> B ) ` y )
25 nfcv 
 |-  F/_ x R
26 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> C ) ` y )
27 24 25 26 nfov 
 |-  F/_ x ( ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y ) )
28 nfcv 
 |-  F/_ y ( ( ( x e. A |-> B ) ` x ) R ( ( x e. A |-> C ) ` x ) )
29 fveq2 
 |-  ( y = x -> ( ( x e. A |-> B ) ` y ) = ( ( x e. A |-> B ) ` x ) )
30 fveq2 
 |-  ( y = x -> ( ( x e. A |-> C ) ` y ) = ( ( x e. A |-> C ) ` x ) )
31 29 30 oveq12d 
 |-  ( y = x -> ( ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y ) ) = ( ( ( x e. A |-> B ) ` x ) R ( ( x e. A |-> C ) ` x ) ) )
32 27 28 31 cbvmpt 
 |-  ( y e. A |-> ( ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y ) ) ) = ( x e. A |-> ( ( ( x e. A |-> B ) ` x ) R ( ( x e. A |-> C ) ` x ) ) )
33 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
34 7 fvmpt2 
 |-  ( ( x e. A /\ B e. W ) -> ( ( x e. A |-> B ) ` x ) = B )
35 33 2 34 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
36 13 fvmpt2 
 |-  ( ( x e. A /\ C e. X ) -> ( ( x e. A |-> C ) ` x ) = C )
37 33 3 36 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> C ) ` x ) = C )
38 35 37 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) R ( ( x e. A |-> C ) ` x ) ) = ( B R C ) )
39 38 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( ( x e. A |-> B ) ` x ) R ( ( x e. A |-> C ) ` x ) ) ) = ( x e. A |-> ( B R C ) ) )
40 32 39 eqtrid 
 |-  ( ph -> ( y e. A |-> ( ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y ) ) ) = ( x e. A |-> ( B R C ) ) )
41 23 40 eqtrd 
 |-  ( ph -> ( F oF R G ) = ( x e. A |-> ( B R C ) ) )