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

Metamath Proof Explorer

Theorem ovmpodf

Description: Alternate deduction version of ovmpo , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses ovmpodf.1 
|- ( ph -> A e. C )
ovmpodf.2 
|- ( ( ph /\ x = A ) -> B e. D )
ovmpodf.3 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )
ovmpodf.4 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = R -> ps ) )
ovmpodf.5 
|- F/_ x F
ovmpodf.6 
|- F/ x ps
ovmpodf.7 
|- F/_ y F
ovmpodf.8 
|- F/ y ps
Assertion ovmpodf 
|- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )

Proof

Step Hyp Ref Expression
1 ovmpodf.1 
 |-  ( ph -> A e. C )
2 ovmpodf.2 
 |-  ( ( ph /\ x = A ) -> B e. D )
3 ovmpodf.3 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )
4 ovmpodf.4 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = R -> ps ) )
5 ovmpodf.5 
 |-  F/_ x F
6 ovmpodf.6 
 |-  F/ x ps
7 ovmpodf.7 
 |-  F/_ y F
8 ovmpodf.8 
 |-  F/ y ps
9 nfv 
 |-  F/ x ph
10 nfmpo1 
 |-  F/_ x ( x e. C , y e. D |-> R )
11 5 10 nfeq 
 |-  F/ x F = ( x e. C , y e. D |-> R )
12 11 6 nfim 
 |-  F/ x ( F = ( x e. C , y e. D |-> R ) -> ps )
13 1 elexd 
 |-  ( ph -> A e. _V )
14 isset 
 |-  ( A e. _V <-> E. x x = A )
15 13 14 sylib 
 |-  ( ph -> E. x x = A )
16 nfv 
 |-  F/ y ( ph /\ x = A )
17 nfmpo2 
 |-  F/_ y ( x e. C , y e. D |-> R )
18 7 17 nfeq 
 |-  F/ y F = ( x e. C , y e. D |-> R )
19 18 8 nfim 
 |-  F/ y ( F = ( x e. C , y e. D |-> R ) -> ps )
20 2 elexd 
 |-  ( ( ph /\ x = A ) -> B e. _V )
21 isset 
 |-  ( B e. _V <-> E. y y = B )
22 20 21 sylib 
 |-  ( ( ph /\ x = A ) -> E. y y = B )
23 oveq 
 |-  ( F = ( x e. C , y e. D |-> R ) -> ( A F B ) = ( A ( x e. C , y e. D |-> R ) B ) )
24 simprl 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> x = A )
25 simprr 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> y = B )
26 24 25 oveq12d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( x ( x e. C , y e. D |-> R ) y ) = ( A ( x e. C , y e. D |-> R ) B ) )
27 1 adantr 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> A e. C )
28 24 27 eqeltrd 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> x e. C )
29 2 adantrr 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> B e. D )
30 25 29 eqeltrd 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> y e. D )
31 eqid 
 |-  ( x e. C , y e. D |-> R ) = ( x e. C , y e. D |-> R )
32 31 ovmpt4g 
 |-  ( ( x e. C /\ y e. D /\ R e. V ) -> ( x ( x e. C , y e. D |-> R ) y ) = R )
33 28 30 3 32 syl3anc 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( x ( x e. C , y e. D |-> R ) y ) = R )
34 26 33 eqtr3d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( A ( x e. C , y e. D |-> R ) B ) = R )
35 34 eqeq2d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = ( A ( x e. C , y e. D |-> R ) B ) <-> ( A F B ) = R ) )
36 35 4 sylbid 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = ( A ( x e. C , y e. D |-> R ) B ) -> ps ) )
37 23 36 syl5 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )
38 37 expr 
 |-  ( ( ph /\ x = A ) -> ( y = B -> ( F = ( x e. C , y e. D |-> R ) -> ps ) ) )
39 16 19 22 38 exlimimdd 
 |-  ( ( ph /\ x = A ) -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )
40 9 12 15 39 exlimdd 
 |-  ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )