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 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

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	nfrexw	⊢ Ⅎ 𝑢 ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑
8		nfv	⊢ Ⅎ 𝑏 𝜑
9		nfsbc1v	⊢ Ⅎ 𝑣 [ 𝑏 / 𝑣 ] 𝜑
10		sbceq1a	⊢ ( 𝑣 = 𝑏 → ( 𝜑 ↔ [ 𝑏 / 𝑣 ] 𝜑 ) )
11	8 9 10	cbvrexw	⊢ ( ∃ 𝑣 ∈ ℕ0 𝜑 ↔ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] 𝜑 )
12		sbceq1a	⊢ ( 𝑢 = 𝑎 → ( [ 𝑏 / 𝑣 ] 𝜑 ↔ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 ) )
13	12	rexbidv	⊢ ( 𝑢 = 𝑎 → ( ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] 𝜑 ↔ ∃ 𝑏 ∈ ℕ0 [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑣 ] 𝜑 ) )
14	11 13	bitrid	⊢ ( 𝑢 = 𝑎 → ( ∃ 𝑣 ∈ ℕ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 ‘ 𝑁 ) )