Metamath Proof Explorer

Theorem 4rexfrabdioph

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