Metamath Proof Explorer

Theorem 7rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, seven 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 )
rexfrabdioph.7 ⊢ 𝐺 = ( 𝐻 + 1 )
Assertion 7rexfrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ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 rexfrabdioph.7 ⊢ 𝐺 = ( 𝐻 + 1 )
8 sbc2rex ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 ↔ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 )
9 sbc4rex ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 ↔ ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
10 9 2rexbii ⊢ ( ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 ↔ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
11 8 10 bitri ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 ↔ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
12 11 sbcbii ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 ↔ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
13 sbc2rex ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 ↔ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
14 sbc4rex ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 ↔ ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
15 14 2rexbii ⊢ ( ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 ↔ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
16 12 13 15 3bitri ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 ↔ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
17 16 rabbii ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 }
18 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
19 1 18 eqeltrid ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ℕ )
20 19 nnnn0d ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ℕ0 )
21 20 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) → 𝑀 ∈ ℕ0 )
22 sbcrot3 ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 )
23 22 sbcbii ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 )
24 sbcrot3 ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 )
25 sbcrot5 ⊢ ( [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
26 25 sbcbii ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
27 sbcrot5 ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
28 26 27 bitri ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
29 28 sbcbii ⊢ ( [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
30 29 sbcbii ⊢ ( [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
31 23 24 30 3bitri ⊢ ( [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
32 31 sbcbii ⊢ ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 )
33 reseq1 ⊢ ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝑀 ) ) → ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) )
34 33 sbccomieg ⊢ ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 )
35 fzssp1 ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... ( 𝑁 + 1 ) )
36 1 oveq2i ⊢ ( 1 ... 𝑀 ) = ( 1 ... ( 𝑁 + 1 ) )
37 35 36 sseqtrri ⊢ ( 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 vex ⊢ 𝑡 ∈ V
42 41 resex ⊢ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ∈ V
43 fveq1 ⊢ ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝑀 ) ) → ( 𝑎 ‘ 𝑀 ) = ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) )
44 43 sbcco3gw ⊢ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ∈ V → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
45 42 44 ax-mp ⊢ ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 )
46 elfz1end ⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( 1 ... 𝑀 ) )
47 19 46 sylib ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ( 1 ... 𝑀 ) )
48 fvres ⊢ ( 𝑀 ∈ ( 1 ... 𝑀 ) → ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) = ( 𝑡 ‘ 𝑀 ) )
49 dfsbcq ⊢ ( ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) = ( 𝑡 ‘ 𝑀 ) → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
50 47 48 49 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
51 45 50 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
52 51 sbcbidv ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
53 40 52 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( ( 𝑡 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
54 34 53 bitrid ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
55 32 54 bitr3id ⊢ ( 𝑁 ∈ ℕ0 → ( [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 ) )
56 55 rabbidv ⊢ ( 𝑁 ∈ ℕ0 → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } )
57 56 eleq1d ⊢ ( 𝑁 ∈ ℕ0 → ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) )
58 57 biimpar ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) )
59 2 3 4 5 6 7 6rexfrabdioph ⊢ ( ( 𝑀 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑀 ) ) / 𝑎 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
60 21 58 59 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
61 17 60 eqeltrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
62 1 rexfrabdioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑎 ‘ 𝑀 ) / 𝑣 ] ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )
63 61 62 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝐺 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ‘ 𝐿 ) / 𝑤 ] [ ( 𝑡 ‘ 𝐾 ) / 𝑥 ] [ ( 𝑡 ‘ 𝐽 ) / 𝑦 ] [ ( 𝑡 ‘ 𝐼 ) / 𝑧 ] [ ( 𝑡 ‘ 𝐻 ) / 𝑝 ] [ ( 𝑡 ‘ 𝐺 ) / 𝑞 ] 𝜑 } ∈ ( Dioph ‘ 𝐺 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 ∃ 𝑧 ∈ ℕ0 ∃ 𝑝 ∈ ℕ0 ∃ 𝑞 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )