Metamath Proof Explorer


Theorem 2rexfrabdioph

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

Ref Expression
Hypotheses rexfrabdioph.1 𝑀 = ( 𝑁 + 1 )
rexfrabdioph.2 𝐿 = ( 𝑀 + 1 )
Assertion 2rexfrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑢 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rexfrabdioph.1 𝑀 = ( 𝑁 + 1 )
2 rexfrabdioph.2 𝐿 = ( 𝑀 + 1 )
3 2sbcrex ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ]𝑤 ∈ ℕ0 𝜑 ↔ ∃ 𝑤 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 )
4 3 rabbii { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ]𝑤 ∈ ℕ0 𝜑 } = { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 }
5 peano2nn0 ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
6 1 5 eqeltrid ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 )
7 6 adantr ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → 𝑀 ∈ ℕ0 )
8 sbcrot3 ( [ ( 𝑡𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑[ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 )
9 8 sbcbii ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 )
10 reseq1 ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝑀 ) ) → ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) )
11 10 sbccomieg ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 )
12 fzssp1 ( 1 ... 𝑁 ) ⊆ ( 1 ... ( 𝑁 + 1 ) )
13 1 oveq2i ( 1 ... 𝑀 ) = ( 1 ... ( 𝑁 + 1 ) )
14 12 13 sseqtrri ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 )
15 resabs1 ( ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) → ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) )
16 dfsbcq ( ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
17 14 15 16 mp2b ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 )
18 vex 𝑡 ∈ V
19 18 resex ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ∈ V
20 fveq1 ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝑀 ) ) → ( 𝑎𝑀 ) = ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) )
21 20 sbcco3gw ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ∈ V → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
22 19 21 ax-mp ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 )
23 nn0p1nn ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
24 1 23 eqeltrid ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ )
25 elfz1end ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( 1 ... 𝑀 ) )
26 24 25 sylib ( 𝑁 ∈ ℕ0𝑀 ∈ ( 1 ... 𝑀 ) )
27 fvres ( 𝑀 ∈ ( 1 ... 𝑀 ) → ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) = ( 𝑡𝑀 ) )
28 dfsbcq ( ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) = ( 𝑡𝑀 ) → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
29 26 27 28 3syl ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
30 22 29 syl5bb ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
31 30 sbcbidv ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
32 17 31 syl5bb ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
33 11 32 syl5bb ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 ) )
34 9 33 bitr2id ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 ) )
35 34 rabbidv ( 𝑁 ∈ ℕ0 → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 } )
36 35 eleq1d ( 𝑁 ∈ ℕ0 → ( { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ↔ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) )
37 36 biimpa ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) )
38 2 rexfrabdioph ( ( 𝑀 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
39 7 37 38 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
40 4 39 eqeltrid ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ]𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
41 1 rexfrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎𝑀 ) / 𝑣 ]𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )
42 40 41 syldan ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] [ ( 𝑡𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑢 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )