Metamath Proof Explorer


Theorem rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypothesis rexfrabdioph.1 𝑀 = ( 𝑁 + 1 )
Assertion rexfrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rexfrabdioph.1 𝑀 = ( 𝑁 + 1 )
2 nfcv 𝑢 ( ℕ0m ( 1 ... 𝑁 ) )
3 nfcv 𝑎 ( ℕ0m ( 1 ... 𝑁 ) )
4 nfv 𝑎𝑣 ∈ ℕ0 𝜑
5 nfcv 𝑢0
6 nfsbc1v 𝑢 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑
7 5 6 nfrex 𝑢𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑
8 nfv 𝑏 𝜑
9 nfsbc1v 𝑣 [ 𝑏 / 𝑣 ] 𝜑
10 sbceq1a ( 𝑣 = 𝑏 → ( 𝜑[ 𝑏 / 𝑣 ] 𝜑 ) )
11 8 9 10 cbvrexw ( ∃ 𝑣 ∈ ℕ0 𝜑 ↔ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] 𝜑 )
12 sbceq1a ( 𝑢 = 𝑎 → ( [ 𝑏 / 𝑣 ] 𝜑[ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 ) )
13 12 rexbidv ( 𝑢 = 𝑎 → ( ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] 𝜑 ↔ ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 ) )
14 11 13 syl5bb ( 𝑢 = 𝑎 → ( ∃ 𝑣 ∈ ℕ0 𝜑 ↔ ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 ) )
15 2 3 4 7 14 cbvrabw { 𝑢 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜑 } = { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 }
16 dfsbcq ( 𝑏 = ( 𝑡𝑀 ) → ( [ 𝑏 / 𝑣 ] 𝜑[ ( 𝑡𝑀 ) / 𝑣 ] 𝜑 ) )
17 16 sbcbidv ( 𝑏 = ( 𝑡𝑀 ) → ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑[ 𝑎 / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] 𝜑 ) )
18 dfsbcq ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ( [ 𝑎 / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] 𝜑[ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] 𝜑 ) )
19 1 17 18 rexrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )
20 15 19 eqeltrid ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )