Step |
Hyp |
Ref |
Expression |
1 |
|
rexfrabdioph.1 |
⊢ 𝑀 = ( 𝑁 + 1 ) |
2 |
|
nfcv |
⊢ Ⅎ 𝑢 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) |
3 |
|
nfcv |
⊢ Ⅎ 𝑎 ( ℕ0 ↑m ( 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 |
⊢ { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜑 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 } |
16 |
|
dfsbcq |
⊢ ( 𝑏 = ( 𝑡 ‘ 𝑀 ) → ( [ 𝑏 / 𝑣 ] 𝜑 ↔ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] 𝜑 ) ) |
17 |
16
|
sbcbidv |
⊢ ( 𝑏 = ( 𝑡 ‘ 𝑀 ) → ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 ↔ [ 𝑎 / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] 𝜑 ) ) |
18 |
|
dfsbcq |
⊢ ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ( [ 𝑎 / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] 𝜑 ↔ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] 𝜑 ) ) |
19 |
1 17 18
|
rexrabdioph |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ) |
20 |
15 19
|
eqeltrid |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ) |