Metamath Proof Explorer

Theorem 6rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, six 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 )
rexfrabdioph.3 ⊢ 𝐾 = ( 𝐿 + 1 )
rexfrabdioph.4 ⊢ 𝐽 = ( 𝐾 + 1 )
rexfrabdioph.5 ⊢ 𝐼 = ( 𝐽 + 1 )
rexfrabdioph.6 ⊢ 𝐻 = ( 𝐼 + 1 )
Assertion 6rexfrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rexfrabdioph.1 ⊢ 𝑀 = ( 𝑁 + 1 )
2 rexfrabdioph.2 ⊢ 𝐿 = ( 𝑀 + 1 )
3 rexfrabdioph.3 ⊢ 𝐾 = ( 𝐿 + 1 )
4 rexfrabdioph.4 ⊢ 𝐽 = ( 𝐾 + 1 )
5 rexfrabdioph.5 ⊢ 𝐼 = ( 𝐽 + 1 )
6 rexfrabdioph.6 ⊢ 𝐻 = ( 𝐼 + 1 )
7 sbc4rex ⊢ ( [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 ↔ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
8 7 sbcbii ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 ↔ [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
9 sbc4rex ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
10 8 9 bitri ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 ↔ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
11 10 sbcbii ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 ↔ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
12 sbc4rex ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
13 11 12 bitri ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 ↔ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
14 13 rabbii ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 }
15 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
16 1 15 eqeltrid ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ℕ )
17 16 peano2nnd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ )
18 2 17 eqeltrid ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 ∈ ℕ )
19 18 nnnn0d ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 ∈ ℕ0 )
20 19 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) → 𝐿 ∈ ℕ0 )
21 sbcrot5 ⊢ ( [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
22 21 sbcbii ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
23 sbcrot5 ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
24 22 23 bitri ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
25 24 sbcbii ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
26 sbcrot5 ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
27 25 26 bitri ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
28 27 sbcbii ⊢ ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 )
29 reseq1 ⊢ ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝐿 ) ) → ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ↾ ( 1 ... 𝑁 ) ) )
30 29 sbccomieg ⊢ ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 )
31 fzssp1 ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... ( 𝑁 + 1 ) )
32 1 oveq2i ⊢ ( 1 ... 𝑀 ) = ( 1 ... ( 𝑁 + 1 ) )
33 31 32 sseqtrri ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 )
34 fzssp1 ⊢ ( 1 ... 𝑀 ) ⊆ ( 1 ... ( 𝑀 + 1 ) )
35 2 oveq2i ⊢ ( 1 ... 𝐿 ) = ( 1 ... ( 𝑀 + 1 ) )
36 34 35 sseqtrri ⊢ ( 1 ... 𝑀 ) ⊆ ( 1 ... 𝐿 )
37 33 36 sstri ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝐿 )
38 resabs1 ⊢ ( ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝐿 ) → ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) )
39 dfsbcq ⊢ ( ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
40 37 38 39 mp2b ⊢ ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 )
41 fveq1 ⊢ ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝐿 ) ) → ( 𝑎 ‘ 𝑀 ) = ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝑀 ) )
42 41 sbccomieg ⊢ ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 )
43 elfz1end ⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( 1 ... 𝑀 ) )
44 16 43 sylib ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ( 1 ... 𝑀 ) )
45 36 44 sselid ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ( 1 ... 𝐿 ) )
46 fvres ⊢ ( 𝑀 ∈ ( 1 ... 𝐿 ) → ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝑀 ) = ( 𝑡 ‘ 𝑀 ) )
47 dfsbcq ⊢ ( ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝑀 ) = ( 𝑡 ‘ 𝑀 ) → ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
48 45 46 47 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
49 vex ⊢ 𝑡 ∈ V
50 49 resex ⊢ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ∈ V
51 fveq1 ⊢ ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝐿 ) ) → ( 𝑎 ‘ 𝐿 ) = ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝐿 ) )
52 51 sbcco3gw ⊢ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ∈ V → ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
53 50 52 ax-mp ⊢ ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 )
54 elfz1end ⊢ ( 𝐿 ∈ ℕ ↔ 𝐿 ∈ ( 1 ... 𝐿 ) )
55 18 54 sylib ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 ∈ ( 1 ... 𝐿 ) )
56 fvres ⊢ ( 𝐿 ∈ ( 1 ... 𝐿 ) → ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝐿 ) = ( 𝑡 ‘ 𝐿 ) )
57 dfsbcq ⊢ ( ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝐿 ) = ( 𝑡 ‘ 𝐿 ) → ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
58 55 56 57 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
59 53 58 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
60 59 sbcbidv ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
61 48 60 bitrd ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
62 42 61 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
63 62 sbcbidv ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
64 40 63 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝐿 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
65 30 64 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
66 28 65 bitr3id ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 ) )
67 66 rabbidv ⊢ ( 𝑁 ∈ ℕ0 → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } )
68 67 eleq1d ⊢ ( 𝑁 ∈ ℕ0 → ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) )
69 68 biimpar ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) )
70 3 4 5 6 4rexfrabdioph ⊢ ( ( 𝐿 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝐿 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) )
71 20 69 70 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] 𝜑 } ∈ ( Dioph ‘ 𝐿 ) )
72 14 71 eqeltrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝐿 ) )
73 1 2 2rexfrabdioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝐿 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑎 ‘ 𝐿 ) / 𝑤 ] ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝐿 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )
74 72 73 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐻 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] 𝜑 } ∈ ( Dioph ‘ 𝐻 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )