Metamath Proof Explorer


Theorem 3rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, two variables. (Contributed by Stefan O'Rear, 17-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses rexfrabdioph.1 M = N + 1
rexfrabdioph.2 L = M + 1
rexfrabdioph.3 K = L + 1
Assertion 3rexfrabdioph N 0 t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ Dioph K u 0 1 N | v 0 w 0 x 0 φ Dioph N

Proof

Step Hyp Ref Expression
1 rexfrabdioph.1 M = N + 1
2 rexfrabdioph.2 L = M + 1
3 rexfrabdioph.3 K = L + 1
4 sbc2rex [˙ a M / v]˙ w 0 x 0 φ w 0 x 0 [˙ a M / v]˙ φ
5 4 sbcbii [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 φ [˙ a 1 N / u]˙ w 0 x 0 [˙ a M / v]˙ φ
6 sbc2rex [˙ a 1 N / u]˙ w 0 x 0 [˙ a M / v]˙ φ w 0 x 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
7 5 6 bitri [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 φ w 0 x 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
8 7 rabbii a 0 1 M | [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 φ = a 0 1 M | w 0 x 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
9 nn0p1nn N 0 N + 1
10 1 9 eqeltrid N 0 M
11 10 nnnn0d N 0 M 0
12 11 adantr N 0 t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ Dioph K M 0
13 sbcrot3 [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a M / v]˙ φ
14 13 sbcbii [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ a 1 N / u]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a M / v]˙ φ
15 sbcrot3 [˙ a 1 N / u]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a M / v]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
16 14 15 bitri [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
17 16 sbcbii [˙ t 1 M / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
18 reseq1 a = t 1 M a 1 N = t 1 M 1 N
19 18 sbccomieg [˙ t 1 M / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
20 fzssp1 1 N 1 N + 1
21 1 oveq2i 1 M = 1 N + 1
22 20 21 sseqtrri 1 N 1 M
23 resabs1 1 N 1 M t 1 M 1 N = t 1 N
24 dfsbcq t 1 M 1 N = t 1 N [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
25 22 23 24 mp2b [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
26 vex t V
27 26 resex t 1 M V
28 fveq1 a = t 1 M a M = t 1 M M
29 28 sbcco3gw t 1 M V [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
30 27 29 ax-mp [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
31 elfz1end M M 1 M
32 10 31 sylib N 0 M 1 M
33 fvres M 1 M t 1 M M = t M
34 dfsbcq t 1 M M = t M [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
35 32 33 34 3syl N 0 [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
36 30 35 syl5bb N 0 [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
37 36 sbcbidv N 0 [˙ t 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
38 25 37 syl5bb N 0 [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
39 19 38 syl5bb N 0 [˙ t 1 M / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
40 17 39 bitr3id N 0 [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
41 40 rabbidv N 0 t 0 1 K | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ = t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ
42 41 eleq1d N 0 t 0 1 K | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph K t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ Dioph K
43 42 biimpar N 0 t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ Dioph K t 0 1 K | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph K
44 2 3 2rexfrabdioph M 0 t 0 1 K | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph K a 0 1 M | w 0 x 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph M
45 12 43 44 syl2anc N 0 t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ Dioph K a 0 1 M | w 0 x 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph M
46 8 45 eqeltrid N 0 t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ Dioph K a 0 1 M | [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 φ Dioph M
47 1 rexfrabdioph N 0 a 0 1 M | [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 φ Dioph M u 0 1 N | v 0 w 0 x 0 φ Dioph N
48 46 47 syldan N 0 t 0 1 K | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ φ Dioph K u 0 1 N | v 0 w 0 x 0 φ Dioph N