Metamath Proof Explorer

Theorem ofrfval2

Description: The function relation acting on maps. (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 ofrfval2 
|- ( ph -> ( F oR R G <-> A. 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 ofrfval 
 |-  ( ph -> ( F oR R G <-> A. 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 nfbr 
 |-  F/ x ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y )
28 nfv 
 |-  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 breq12d 
 |-  ( 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 cbvralw 
 |-  ( A. y e. A ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y ) <-> A. 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 breq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) R ( ( x e. A |-> C ) ` x ) <-> B R C ) )
39 38 ralbidva 
 |-  ( ph -> ( A. x e. A ( ( x e. A |-> B ) ` x ) R ( ( x e. A |-> C ) ` x ) <-> A. x e. A B R C ) )
40 32 39 syl5bb 
 |-  ( ph -> ( A. y e. A ( ( x e. A |-> B ) ` y ) R ( ( x e. A |-> C ) ` y ) <-> A. x e. A B R C ) )
41 23 40 bitrd 
 |-  ( ph -> ( F oR R G <-> A. x e. A B R C ) )