Metamath Proof Explorer

Theorem ovmpodxf

Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses ovmpodx.1 
|- ( ph -> F = ( x e. C , y e. D |-> R ) )
ovmpodx.2 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
ovmpodx.3 
|- ( ( ph /\ x = A ) -> D = L )
ovmpodx.4 
|- ( ph -> A e. C )
ovmpodx.5 
|- ( ph -> B e. L )
ovmpodx.6 
|- ( ph -> S e. X )
ovmpodxf.px 
|- F/ x ph
ovmpodxf.py 
|- F/ y ph
ovmpodxf.ay 
|- F/_ y A
ovmpodxf.bx 
|- F/_ x B
ovmpodxf.sx 
|- F/_ x S
ovmpodxf.sy 
|- F/_ y S
Assertion ovmpodxf 
|- ( ph -> ( A F B ) = S )

Proof

Step Hyp Ref Expression
1 ovmpodx.1 
 |-  ( ph -> F = ( x e. C , y e. D |-> R ) )
2 ovmpodx.2 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
3 ovmpodx.3 
 |-  ( ( ph /\ x = A ) -> D = L )
4 ovmpodx.4 
 |-  ( ph -> A e. C )
5 ovmpodx.5 
 |-  ( ph -> B e. L )
6 ovmpodx.6 
 |-  ( ph -> S e. X )
7 ovmpodxf.px 
 |-  F/ x ph
8 ovmpodxf.py 
 |-  F/ y ph
9 ovmpodxf.ay 
 |-  F/_ y A
10 ovmpodxf.bx 
 |-  F/_ x B
11 ovmpodxf.sx 
 |-  F/_ x S
12 ovmpodxf.sy 
 |-  F/_ y S
13 1 oveqd 
 |-  ( ph -> ( A F B ) = ( A ( x e. C , y e. D |-> R ) B ) )
14 eqid 
 |-  ( x e. C , y e. D |-> R ) = ( x e. C , y e. D |-> R )
15 14 ovmpt4g 
 |-  ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R )
16 15 a1i 
 |-  ( ph -> ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) )
17 8 16 alrimi 
 |-  ( ph -> A. y ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) )
18 5 17 spsbcd 
 |-  ( ph -> [. B / y ]. ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) )
19 7 18 alrimi 
 |-  ( ph -> A. x [. B / y ]. ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) )
20 4 19 spsbcd 
 |-  ( ph -> [. A / x ]. [. B / y ]. ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) )
21 5 adantr 
 |-  ( ( ph /\ x = A ) -> B e. L )
22 simplr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> x = A )
23 4 ad2antrr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> A e. C )
24 22 23 eqeltrd 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> x e. C )
25 5 ad2antrr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> B e. L )
26 simpr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> y = B )
27 3 adantr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> D = L )
28 25 26 27 3eltr4d 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> y e. D )
29 2 anassrs 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> R = S )
30 6 elexd 
 |-  ( ph -> S e. _V )
31 30 ad2antrr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> S e. _V )
32 29 31 eqeltrd 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> R e. _V )
33 biimt 
 |-  ( ( x e. C /\ y e. D /\ R e. _V ) -> ( ( x ( x e. C , y e. D |-> R ) y ) = R <-> ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) ) )
34 24 28 32 33 syl3anc 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( ( x ( x e. C , y e. D |-> R ) y ) = R <-> ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) ) )
35 22 26 oveq12d 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( x ( x e. C , y e. D |-> R ) y ) = ( A ( x e. C , y e. D |-> R ) B ) )
36 35 29 eqeq12d 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( ( x ( x e. C , y e. D |-> R ) y ) = R <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
37 34 36 bitr3d 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
38 9 nfeq2 
 |-  F/ y x = A
39 8 38 nfan 
 |-  F/ y ( ph /\ x = A )
40 nfmpo2 
 |-  F/_ y ( x e. C , y e. D |-> R )
41 nfcv 
 |-  F/_ y B
42 9 40 41 nfov 
 |-  F/_ y ( A ( x e. C , y e. D |-> R ) B )
43 42 12 nfeq 
 |-  F/ y ( A ( x e. C , y e. D |-> R ) B ) = S
44 43 a1i 
 |-  ( ( ph /\ x = A ) -> F/ y ( A ( x e. C , y e. D |-> R ) B ) = S )
45 21 37 39 44 sbciedf 
 |-  ( ( ph /\ x = A ) -> ( [. B / y ]. ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
46 nfcv 
 |-  F/_ x A
47 nfmpo1 
 |-  F/_ x ( x e. C , y e. D |-> R )
48 46 47 10 nfov 
 |-  F/_ x ( A ( x e. C , y e. D |-> R ) B )
49 48 11 nfeq 
 |-  F/ x ( A ( x e. C , y e. D |-> R ) B ) = S
50 49 a1i 
 |-  ( ph -> F/ x ( A ( x e. C , y e. D |-> R ) B ) = S )
51 4 45 7 50 sbciedf 
 |-  ( ph -> ( [. A / x ]. [. B / y ]. ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
52 20 51 mpbid 
 |-  ( ph -> ( A ( x e. C , y e. D |-> R ) B ) = S )
53 13 52 eqtrd 
 |-  ( ph -> ( A F B ) = S )