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

Metamath Proof Explorer

Theorem offval2f

Description: The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017)

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

Proof

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