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 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 𝜑 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 }
5 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
6 1 5 eqeltrid ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ℕ0 )
7 6 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 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 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ) )
31 30 sbcbidv ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ) )
32 17 31 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ) )
33 11 32 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ) )
34 9 33 bitr2id ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 ) )
35 34 rabbidv ⊢ ( 𝑁 ∈ ℕ0 → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } )
36 35 eleq1d ⊢ ( 𝑁 ∈ ℕ0 → ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) )
37 36 biimpa ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) )
38 2 rexfrabdioph ⊢ ( ( 𝑀 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
39 7 37 38 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
40 4 39 eqeltrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
41 1 rexfrabdioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )
42 40 41 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )