Metamath Proof Explorer

Theorem ovmpordxf

Description: Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf . (Contributed by AV, 30-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 ovmpordx.1 
 |-  ( ph -> F = ( x e. C , y e. D |-> R ) )
2 ovmpordx.2 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
3 ovmpordx.3 
 |-  ( ( ph /\ y = B ) -> C = L )
4 ovmpordx.4 
 |-  ( ph -> A e. L )
5 ovmpordx.5 
 |-  ( ph -> B e. D )
6 ovmpordx.6 
 |-  ( ph -> S e. X )
7 ovmpordxf.px 
 |-  F/ x ph
8 ovmpordxf.py 
 |-  F/ y ph
9 ovmpordxf.ay 
 |-  F/_ y A
10 ovmpordxf.bx 
 |-  F/_ x B
11 ovmpordxf.sx 
 |-  F/_ x S
12 ovmpordxf.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. X ) -> ( x ( x e. C , y e. D |-> R ) y ) = R )
16 15 a1i 
 |-  ( ph -> ( ( x e. C /\ y e. D /\ R e. X ) -> ( 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. X ) -> ( 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. X ) -> ( 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. X ) -> ( 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. X ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) )
21 5 adantr 
 |-  ( ( ph /\ x = A ) -> B e. D )
22 4 ad2antrr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> A e. L )
23 simpr 
 |-  ( ( ph /\ x = A ) -> x = A )
24 23 adantr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> x = A )
25 3 adantlr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> C = L )
26 22 24 25 3eltr4d 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> x e. C )
27 5 ad2antrr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> B e. D )
28 eleq1 
 |-  ( y = B -> ( y e. D <-> B e. D ) )
29 28 adantl 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( y e. D <-> B e. D ) )
30 27 29 mpbird 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> y e. D )
31 2 anassrs 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> R = S )
32 6 ad2antrr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> S e. X )
33 31 32 eqeltrd 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> R e. X )
34 biimt 
 |-  ( ( x e. C /\ y e. D /\ R e. X ) -> ( ( x ( x e. C , y e. D |-> R ) y ) = R <-> ( ( x e. C /\ y e. D /\ R e. X ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) ) )
35 26 30 33 34 syl3anc 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( ( x ( x e. C , y e. D |-> R ) y ) = R <-> ( ( x e. C /\ y e. D /\ R e. X ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) ) )
36 simpr 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> y = B )
37 24 36 oveq12d 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( x ( x e. C , y e. D |-> R ) y ) = ( A ( x e. C , y e. D |-> R ) B ) )
38 37 31 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 ) )
39 35 38 bitr3d 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( ( ( x e. C /\ y e. D /\ R e. X ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
40 9 nfeq2 
 |-  F/ y x = A
41 8 40 nfan 
 |-  F/ y ( ph /\ x = A )
42 nfmpo2 
 |-  F/_ y ( x e. C , y e. D |-> R )
43 nfcv 
 |-  F/_ y B
44 9 42 43 nfov 
 |-  F/_ y ( A ( x e. C , y e. D |-> R ) B )
45 44 12 nfeq 
 |-  F/ y ( A ( x e. C , y e. D |-> R ) B ) = S
46 45 a1i 
 |-  ( ( ph /\ x = A ) -> F/ y ( A ( x e. C , y e. D |-> R ) B ) = S )
47 21 39 41 46 sbciedf 
 |-  ( ( ph /\ x = A ) -> ( [. B / y ]. ( ( x e. C /\ y e. D /\ R e. X ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
48 nfcv 
 |-  F/_ x A
49 nfmpo1 
 |-  F/_ x ( x e. C , y e. D |-> R )
50 48 49 10 nfov 
 |-  F/_ x ( A ( x e. C , y e. D |-> R ) B )
51 50 11 nfeq 
 |-  F/ x ( A ( x e. C , y e. D |-> R ) B ) = S
52 51 a1i 
 |-  ( ph -> F/ x ( A ( x e. C , y e. D |-> R ) B ) = S )
53 4 47 7 52 sbciedf 
 |-  ( ph -> ( [. A / x ]. [. B / y ]. ( ( x e. C /\ y e. D /\ R e. X ) -> ( x ( x e. C , y e. D |-> R ) y ) = R ) <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
54 20 53 mpbid 
 |-  ( ph -> ( A ( x e. C , y e. D |-> R ) B ) = S )
55 13 54 eqtrd 
 |-  ( ph -> ( A F B ) = S )