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 
|- M = ( N + 1 )
Assertion rexfrabdioph 
|- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. ph } e. ( Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ph } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 rexfrabdioph.1 
 |-  M = ( N + 1 )
2 nfcv 
 |-  F/_ u ( NN0 ^m ( 1 ... N ) )
3 nfcv 
 |-  F/_ a ( NN0 ^m ( 1 ... N ) )
4 nfv 
 |-  F/ a E. v e. NN0 ph
5 nfcv 
 |-  F/_ u NN0
6 nfsbc1v 
 |-  F/ u [. a / u ]. [. b / v ]. ph
7 5 6 nfrexw 
 |-  F/ u E. b e. NN0 [. a / u ]. [. b / v ]. ph
8 nfv 
 |-  F/ b ph
9 nfsbc1v 
 |-  F/ v [. b / v ]. ph
10 sbceq1a 
 |-  ( v = b -> ( ph <-> [. b / v ]. ph ) )
11 8 9 10 cbvrexw 
 |-  ( E. v e. NN0 ph <-> E. b e. NN0 [. b / v ]. ph )
12 sbceq1a 
 |-  ( u = a -> ( [. b / v ]. ph <-> [. a / u ]. [. b / v ]. ph ) )
13 12 rexbidv 
 |-  ( u = a -> ( E. b e. NN0 [. b / v ]. ph <-> E. b e. NN0 [. a / u ]. [. b / v ]. ph ) )
14 11 13 bitrid 
 |-  ( u = a -> ( E. v e. NN0 ph <-> E. b e. NN0 [. a / u ]. [. b / v ]. ph ) )
15 2 3 4 7 14 cbvrabw 
 |-  { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ph } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 [. a / u ]. [. b / v ]. ph }
16 dfsbcq 
 |-  ( b = ( t ` M ) -> ( [. b / v ]. ph <-> [. ( t ` M ) / v ]. ph ) )
17 16 sbcbidv 
 |-  ( b = ( t ` M ) -> ( [. a / u ]. [. b / v ]. ph <-> [. a / u ]. [. ( t ` M ) / v ]. ph ) )
18 dfsbcq 
 |-  ( a = ( t |` ( 1 ... N ) ) -> ( [. a / u ]. [. ( t ` M ) / v ]. ph <-> [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. ph ) )
19 1 17 18 rexrabdioph 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. ph } e. ( Dioph ` M ) ) -> { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 [. a / u ]. [. b / v ]. ph } e. ( Dioph ` N ) )
20 15 19 eqeltrid 
 |-  ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. ph } e. ( Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ph } e. ( Dioph ` N ) )