# 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 ${⊢}{\phi }\to {A}\in {C}$
ovmpodf.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to {B}\in {D}$
ovmpodf.3 ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {R}\in {V}$
ovmpodf.4 ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to \left({A}{F}{B}={R}\to {\psi }\right)$
ovmpodf.5 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
ovmpodf.6 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
ovmpodf.7 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{F}$
ovmpodf.8 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion ovmpodf ${⊢}{\phi }\to \left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 ovmpodf.1 ${⊢}{\phi }\to {A}\in {C}$
2 ovmpodf.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to {B}\in {D}$
3 ovmpodf.3 ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {R}\in {V}$
4 ovmpodf.4 ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to \left({A}{F}{B}={R}\to {\psi }\right)$
5 ovmpodf.5 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
6 ovmpodf.6 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
7 ovmpodf.7 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{F}$
8 ovmpodf.8 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
9 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
10 nfmpo1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {C},{y}\in {D}⟼{R}\right)$
11 5 10 nfeq ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)$
12 11 6 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {\psi }\right)$
13 1 elexd ${⊢}{\phi }\to {A}\in \mathrm{V}$
14 isset ${⊢}{A}\in \mathrm{V}↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
15 13 14 sylib ${⊢}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
16 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}={A}\right)$
17 nfmpo2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {C},{y}\in {D}⟼{R}\right)$
18 7 17 nfeq ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)$
19 18 8 nfim ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {\psi }\right)$
20 2 elexd ${⊢}\left({\phi }\wedge {x}={A}\right)\to {B}\in \mathrm{V}$
21 isset ${⊢}{B}\in \mathrm{V}↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}={B}$
22 20 21 sylib ${⊢}\left({\phi }\wedge {x}={A}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}={B}$
23 oveq ${⊢}{F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {A}{F}{B}={A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}$
24 simprl ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {x}={A}$
25 simprr ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {y}={B}$
26 24 25 oveq12d ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {x}\left({x}\in {C},{y}\in {D}⟼{R}\right){y}={A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}$
27 1 adantr ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {A}\in {C}$
28 24 27 eqeltrd ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {x}\in {C}$
29 2 adantrr ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {B}\in {D}$
30 25 29 eqeltrd ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {y}\in {D}$
31 eqid ${⊢}\left({x}\in {C},{y}\in {D}⟼{R}\right)=\left({x}\in {C},{y}\in {D}⟼{R}\right)$
32 31 ovmpt4g ${⊢}\left({x}\in {C}\wedge {y}\in {D}\wedge {R}\in {V}\right)\to {x}\left({x}\in {C},{y}\in {D}⟼{R}\right){y}={R}$
33 28 30 3 32 syl3anc ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {x}\left({x}\in {C},{y}\in {D}⟼{R}\right){y}={R}$
34 26 33 eqtr3d ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={R}$
35 34 eqeq2d ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to \left({A}{F}{B}={A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}↔{A}{F}{B}={R}\right)$
36 35 4 sylbid ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to \left({A}{F}{B}={A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}\to {\psi }\right)$
37 23 36 syl5 ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to \left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {\psi }\right)$
38 37 expr ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left({y}={B}\to \left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {\psi }\right)\right)$
39 16 19 22 38 exlimimdd ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {\psi }\right)$
40 9 12 15 39 exlimdd ${⊢}{\phi }\to \left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {\psi }\right)$