Metamath Proof Explorer

Theorem ovmpos

Description: Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypothesis ovmpos.3 
|- F = ( x e. C , y e. D |-> R )
Assertion ovmpos 
|- ( ( A e. C /\ B e. D /\ [_ A / x ]_ [_ B / y ]_ R e. V ) -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R )

Proof

Step Hyp Ref Expression
1 ovmpos.3 
 |-  F = ( x e. C , y e. D |-> R )
2 elex 
 |-  ( [_ A / x ]_ [_ B / y ]_ R e. V -> [_ A / x ]_ [_ B / y ]_ R e. _V )
3 nfcv 
 |-  F/_ x A
4 nfcv 
 |-  F/_ y A
5 nfcv 
 |-  F/_ y B
6 nfcsb1v 
 |-  F/_ x [_ A / x ]_ R
7 6 nfel1 
 |-  F/ x [_ A / x ]_ R e. _V
8 nfmpo1 
 |-  F/_ x ( x e. C , y e. D |-> R )
9 1 8 nfcxfr 
 |-  F/_ x F
10 nfcv 
 |-  F/_ x y
11 3 9 10 nfov 
 |-  F/_ x ( A F y )
12 11 6 nfeq 
 |-  F/ x ( A F y ) = [_ A / x ]_ R
13 7 12 nfim 
 |-  F/ x ( [_ A / x ]_ R e. _V -> ( A F y ) = [_ A / x ]_ R )
14 nfcsb1v 
 |-  F/_ y [_ B / y ]_ [_ A / x ]_ R
15 14 nfel1 
 |-  F/ y [_ B / y ]_ [_ A / x ]_ R e. _V
16 nfmpo2 
 |-  F/_ y ( x e. C , y e. D |-> R )
17 1 16 nfcxfr 
 |-  F/_ y F
18 4 17 5 nfov 
 |-  F/_ y ( A F B )
19 18 14 nfeq 
 |-  F/ y ( A F B ) = [_ B / y ]_ [_ A / x ]_ R
20 15 19 nfim 
 |-  F/ y ( [_ B / y ]_ [_ A / x ]_ R e. _V -> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R )
21 csbeq1a 
 |-  ( x = A -> R = [_ A / x ]_ R )
22 21 eleq1d 
 |-  ( x = A -> ( R e. _V <-> [_ A / x ]_ R e. _V ) )
23 oveq1 
 |-  ( x = A -> ( x F y ) = ( A F y ) )
24 23 21 eqeq12d 
 |-  ( x = A -> ( ( x F y ) = R <-> ( A F y ) = [_ A / x ]_ R ) )
25 22 24 imbi12d 
 |-  ( x = A -> ( ( R e. _V -> ( x F y ) = R ) <-> ( [_ A / x ]_ R e. _V -> ( A F y ) = [_ A / x ]_ R ) ) )
26 csbeq1a 
 |-  ( y = B -> [_ A / x ]_ R = [_ B / y ]_ [_ A / x ]_ R )
27 26 eleq1d 
 |-  ( y = B -> ( [_ A / x ]_ R e. _V <-> [_ B / y ]_ [_ A / x ]_ R e. _V ) )
28 oveq2 
 |-  ( y = B -> ( A F y ) = ( A F B ) )
29 28 26 eqeq12d 
 |-  ( y = B -> ( ( A F y ) = [_ A / x ]_ R <-> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) )
30 27 29 imbi12d 
 |-  ( y = B -> ( ( [_ A / x ]_ R e. _V -> ( A F y ) = [_ A / x ]_ R ) <-> ( [_ B / y ]_ [_ A / x ]_ R e. _V -> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) ) )
31 1 ovmpt4g 
 |-  ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x F y ) = R )
32 31 3expia 
 |-  ( ( x e. C /\ y e. D ) -> ( R e. _V -> ( x F y ) = R ) )
33 3 4 5 13 20 25 30 32 vtocl2gaf 
 |-  ( ( A e. C /\ B e. D ) -> ( [_ B / y ]_ [_ A / x ]_ R e. _V -> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) )
34 csbcom 
 |-  [_ A / x ]_ [_ B / y ]_ R = [_ B / y ]_ [_ A / x ]_ R
35 34 eleq1i 
 |-  ( [_ A / x ]_ [_ B / y ]_ R e. _V <-> [_ B / y ]_ [_ A / x ]_ R e. _V )
36 34 eqeq2i 
 |-  ( ( A F B ) = [_ A / x ]_ [_ B / y ]_ R <-> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R )
37 33 35 36 3imtr4g 
 |-  ( ( A e. C /\ B e. D ) -> ( [_ A / x ]_ [_ B / y ]_ R e. _V -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R ) )
38 2 37 syl5 
 |-  ( ( A e. C /\ B e. D ) -> ( [_ A / x ]_ [_ B / y ]_ R e. V -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R ) )
39 38 3impia 
 |-  ( ( A e. C /\ B e. D /\ [_ A / x ]_ [_ B / y ]_ R e. V ) -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R )