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 M ψ χ
rexrabdioph.3 u = t 1 N χ φ
Assertion rexrabdioph N 0 t 0 1 M | φ Dioph M u 0 1 N | v 0 ψ Dioph N

Proof

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