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 ⊢ 𝑀 = ( 𝑁 + 1 )
rexfrabdioph.2 ⊢ 𝐿 = ( 𝑀 + 1 )
rexfrabdioph.3 ⊢ 𝐾 = ( 𝐿 + 1 )
Assertion 3rexfrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] 𝜑 } ∈ ( Dioph ‘ 𝐾 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

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