# Metamath Proof Explorer

## Theorem rexrabdioph

Description: Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Hypotheses rexrabdioph.1 ${⊢}{M}={N}+1$
rexrabdioph.2 ${⊢}{v}={t}\left({M}\right)\to \left({\psi }↔{\chi }\right)$
rexrabdioph.3 ${⊢}{u}={{t}↾}_{\left(1\dots {N}\right)}\to \left({\chi }↔{\phi }\right)$
Assertion rexrabdioph ${⊢}\left({N}\in {ℕ}_{0}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to \left\{{u}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)|\exists {v}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\psi }\right\}\in \mathrm{Dioph}\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 rexrabdioph.1 ${⊢}{M}={N}+1$
2 rexrabdioph.2 ${⊢}{v}={t}\left({M}\right)\to \left({\psi }↔{\chi }\right)$
3 rexrabdioph.3 ${⊢}{u}={{t}↾}_{\left(1\dots {N}\right)}\to \left({\chi }↔{\phi }\right)$
4 df-rab
5 dfsbcq
6 5 cbvrexvw
7 6 anbi2i
8 r19.42v
9 7 8 bitr4i
10 simpll ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to {N}\in {ℕ}_{0}$
11 simpr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)$
12 simplr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to {c}\in {ℕ}_{0}$
13 1 mapfzcons ${⊢}\left({N}\in {ℕ}_{0}\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\wedge {c}\in {ℕ}_{0}\right)\to {a}\cup \left\{⟨{M},{c}⟩\right\}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)$
14 10 11 12 13 syl3anc ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to {a}\cup \left\{⟨{M},{c}⟩\right\}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)$
16 1 mapfzcons2 ${⊢}\left({a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\wedge {c}\in {ℕ}_{0}\right)\to \left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)\left({M}\right)={c}$
17 11 12 16 syl2anc ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to \left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)\left({M}\right)={c}$
18 17 eqcomd ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to {c}=\left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)\left({M}\right)$
19 1 mapfzcons1 ${⊢}{a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\to {\left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)↾}_{\left(1\dots {N}\right)}={a}$
20 19 adantl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to {\left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)↾}_{\left(1\dots {N}\right)}={a}$
21 20 eqcomd ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {c}\in {ℕ}_{0}\right)\wedge {a}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)\right)\to {a}={\left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)↾}_{\left(1\dots {N}\right)}$
22 21 sbceq1d
23 18 22 sbceqbid
24 23 biimpd
25 24 impr
27 fveq1 ${⊢}{b}={a}\cup \left\{⟨{M},{c}⟩\right\}\to {b}\left({M}\right)=\left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)\left({M}\right)$
28 reseq1 ${⊢}{b}={a}\cup \left\{⟨{M},{c}⟩\right\}\to {{b}↾}_{\left(1\dots {N}\right)}={\left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)↾}_{\left(1\dots {N}\right)}$
29 28 sbceq1d
30 27 29 sbceqbid
31 28 eqeq2d ${⊢}{b}={a}\cup \left\{⟨{M},{c}⟩\right\}\to \left({a}={{b}↾}_{\left(1\dots {N}\right)}↔{a}={\left({a}\cup \left\{⟨{M},{c}⟩\right\}\right)↾}_{\left(1\dots {N}\right)}\right)$
32 30 31 anbi12d
33 32 rspcev
34 15 25 26 33 syl12anc
35 34 rexlimdva2
36 elmapi ${⊢}{b}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)\to {b}:\left(1\dots {M}\right)⟶{ℕ}_{0}$
37 nn0p1nn ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in ℕ$
38 1 37 eqeltrid ${⊢}{N}\in {ℕ}_{0}\to {M}\in ℕ$
39 elfz1end ${⊢}{M}\in ℕ↔{M}\in \left(1\dots {M}\right)$
40 38 39 sylib ${⊢}{N}\in {ℕ}_{0}\to {M}\in \left(1\dots {M}\right)$
41 ffvelrn ${⊢}\left({b}:\left(1\dots {M}\right)⟶{ℕ}_{0}\wedge {M}\in \left(1\dots {M}\right)\right)\to {b}\left({M}\right)\in {ℕ}_{0}$
42 36 40 41 syl2anr ${⊢}\left({N}\in {ℕ}_{0}\wedge {b}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)\right)\to {b}\left({M}\right)\in {ℕ}_{0}$
44 simprr
45 1 mapfzcons1cl ${⊢}{b}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)\to {{b}↾}_{\left(1\dots {N}\right)}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)$
47 44 46 eqeltrd
48 simprl
49 dfsbcq
50 49 sbcbidv
52 48 51 mpbird
53 dfsbcq
54 53 anbi2d
55 54 rspcev
56 43 47 52 55 syl12anc
57 56 rexlimdva2
58 35 57 impbid
59 9 58 syl5bb
60 59 abbidv
61 4 60 syl5eq
62 nfcv ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}\left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)$
63 nfcv ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}\left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)$
64 nfv ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}\exists {v}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\psi }$
65 nfcv ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}{ℕ}_{0}$
66 nfcv ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}{b}$
67 nfsbc1v
68 66 67 nfsbcw
69 65 68 nfrex
70 sbceq1a
71 70 rexbidv
72 nfv
73 nfsbc1v
74 sbceq1a
75 72 73 74 cbvrexw
76 71 75 syl6bb
77 62 63 64 69 76 cbvrabw
78 fveq1 ${⊢}{t}={b}\to {t}\left({M}\right)={b}\left({M}\right)$
79 reseq1 ${⊢}{t}={b}\to {{t}↾}_{\left(1\dots {N}\right)}={{b}↾}_{\left(1\dots {N}\right)}$
80 79 sbceq1d
81 78 80 sbceqbid
82 81 rexrab
83 82 abbii
84 61 77 83 3eqtr4g
85 fvex ${⊢}{t}\left({M}\right)\in \mathrm{V}$
86 vex ${⊢}{t}\in \mathrm{V}$
87 86 resex ${⊢}{{t}↾}_{\left(1\dots {N}\right)}\in \mathrm{V}$
88 2 3 sylan9bb ${⊢}\left({v}={t}\left({M}\right)\wedge {u}={{t}↾}_{\left(1\dots {N}\right)}\right)\to \left({\psi }↔{\phi }\right)$
89 85 87 88 sbc2ie
90 89 rabbii
91 90 rexeqi
92 91 abbii
93 84 92 syl6eq ${⊢}{N}\in {ℕ}_{0}\to \left\{{u}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)|\exists {v}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\psi }\right\}=\left\{{a}|\exists {b}\in \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{a}={{b}↾}_{\left(1\dots {N}\right)}\right\}$
94 93 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to \left\{{u}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)|\exists {v}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\psi }\right\}=\left\{{a}|\exists {b}\in \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{a}={{b}↾}_{\left(1\dots {N}\right)}\right\}$
95 simpl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to {N}\in {ℕ}_{0}$
96 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
97 uzid ${⊢}{N}\in ℤ\to {N}\in {ℤ}_{\ge {N}}$
98 peano2uz ${⊢}{N}\in {ℤ}_{\ge {N}}\to {N}+1\in {ℤ}_{\ge {N}}$
99 96 97 98 3syl ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in {ℤ}_{\ge {N}}$
100 1 99 eqeltrid ${⊢}{N}\in {ℕ}_{0}\to {M}\in {ℤ}_{\ge {N}}$
101 100 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to {M}\in {ℤ}_{\ge {N}}$
102 simpr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)$
103 diophrex ${⊢}\left({N}\in {ℕ}_{0}\wedge {M}\in {ℤ}_{\ge {N}}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to \left\{{a}|\exists {b}\in \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{a}={{b}↾}_{\left(1\dots {N}\right)}\right\}\in \mathrm{Dioph}\left({N}\right)$
104 95 101 102 103 syl3anc ${⊢}\left({N}\in {ℕ}_{0}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to \left\{{a}|\exists {b}\in \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{a}={{b}↾}_{\left(1\dots {N}\right)}\right\}\in \mathrm{Dioph}\left({N}\right)$
105 94 104 eqeltrd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left\{{t}\in \left({{ℕ}_{0}}^{\left(1\dots {M}\right)}\right)|{\phi }\right\}\in \mathrm{Dioph}\left({M}\right)\right)\to \left\{{u}\in \left({{ℕ}_{0}}^{\left(1\dots {N}\right)}\right)|\exists {v}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\psi }\right\}\in \mathrm{Dioph}\left({N}\right)$