Metamath Proof Explorer

Theorem rexrabdioph

Description: Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Hypotheses rexrabdioph.1 ⊢ 𝑀 = ( 𝑁 + 1 )
rexrabdioph.2 ⊢ ( 𝑣 = ( 𝑡 ‘ 𝑀 ) → ( 𝜓 ↔ 𝜒 ) )
rexrabdioph.3 ⊢ ( 𝑢 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ( 𝜒 ↔ 𝜑 ) )
Assertion rexrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜓 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rexrabdioph.1 ⊢ 𝑀 = ( 𝑁 + 1 )
2 rexrabdioph.2 ⊢ ( 𝑣 = ( 𝑡 ‘ 𝑀 ) → ( 𝜓 ↔ 𝜒 ) )
3 rexrabdioph.3 ⊢ ( 𝑢 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ( 𝜒 ↔ 𝜑 ) )
4 df-rab ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 } = { 𝑎 ∣ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) }
5 dfsbcq ⊢ ( 𝑏 = 𝑐 → ( [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ↔ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
6 5 cbvrexvw ⊢ ( ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ↔ ∃ 𝑐 ∈ ℕ0 [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 )
7 6 anbi2i ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ↔ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑐 ∈ ℕ0 [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
8 r19.42v ⊢ ( ∃ 𝑐 ∈ ℕ0 ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ↔ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑐 ∈ ℕ0 [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
9 7 8 bitr4i ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ↔ ∃ 𝑐 ∈ ℕ0 ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
10 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
11 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
12 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝑐 ∈ ℕ0 )
13 1 mapfzcons ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) )
14 10 11 12 13 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) )
15 14 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ) → ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) )
16 1 mapfzcons2 ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) = 𝑐 )
17 11 12 16 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) = 𝑐 )
18 17 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝑐 = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) )
19 1 mapfzcons1 ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) = 𝑎 )
20 19 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) = 𝑎 )
21 20 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝑎 = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) )
22 21 sbceq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( [ 𝑎 / 𝑢 ] 𝜓 ↔ [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
23 18 22 sbceqbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ↔ [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) / 𝑣 ] [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
24 23 biimpd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 → [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) / 𝑣 ] [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
25 24 impr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ) → [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) / 𝑣 ] [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 )
26 21 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ) → 𝑎 = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) )
27 fveq1 ⊢ ( 𝑏 = ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) → ( 𝑏 ‘ 𝑀 ) = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) )
28 reseq1 ⊢ ( 𝑏 = ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) )
29 28 sbceq1d ⊢ ( 𝑏 = ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) → ( [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ↔ [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
30 27 29 sbceqbid ⊢ ( 𝑏 = ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) → ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ↔ [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) / 𝑣 ] [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
31 28 eqeq2d ⊢ ( 𝑏 = ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) → ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑎 = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) ) )
32 30 31 anbi12d ⊢ ( 𝑏 = ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) → ( ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ( [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) / 𝑣 ] [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) ) ) )
33 32 rspcev ⊢ ( ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ ( [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ‘ 𝑀 ) / 𝑣 ] [ ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( ( 𝑎 ∪ { ⟨ 𝑀 , 𝑐 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) ) ) → ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
34 15 25 26 33 syl12anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ) → ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
35 34 rexlimdva2 ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑐 ∈ ℕ0 ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) → ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) )
36 elmapi ⊢ ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) → 𝑏 : ( 1 ... 𝑀 ) ⟶ ℕ0 )
37 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
38 1 37 eqeltrid ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ℕ )
39 elfz1end ⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( 1 ... 𝑀 ) )
40 38 39 sylib ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ( 1 ... 𝑀 ) )
41 ffvelrn ⊢ ( ( 𝑏 : ( 1 ... 𝑀 ) ⟶ ℕ0 ∧ 𝑀 ∈ ( 1 ... 𝑀 ) ) → ( 𝑏 ‘ 𝑀 ) ∈ ℕ0 )
42 36 40 41 syl2anr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) → ( 𝑏 ‘ 𝑀 ) ∈ ℕ0 )
43 42 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑏 ‘ 𝑀 ) ∈ ℕ0 )
44 simprr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) )
45 1 mapfzcons1cl ⊢ ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
46 45 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
47 44 46 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
48 simprl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 )
49 dfsbcq ⊢ ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) → ( [ 𝑎 / 𝑢 ] 𝜓 ↔ [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
50 49 sbcbidv ⊢ ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) → ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ↔ [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
51 50 ad2antll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ↔ [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
52 48 51 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 )
53 dfsbcq ⊢ ( 𝑐 = ( 𝑏 ‘ 𝑀 ) → ( [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ↔ [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
54 53 anbi2d ⊢ ( 𝑐 = ( 𝑏 ‘ 𝑀 ) → ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ↔ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ) )
55 54 rspcev ⊢ ( ( ( 𝑏 ‘ 𝑀 ) ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ) → ∃ 𝑐 ∈ ℕ0 ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
56 43 47 52 55 syl12anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) → ∃ 𝑐 ∈ ℕ0 ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
57 56 rexlimdva2 ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) → ∃ 𝑐 ∈ ℕ0 ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ) )
58 35 57 impbid ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑐 ∈ ℕ0 ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ [ 𝑐 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) )
59 9 58 syl5bb ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) )
60 59 abbidv ⊢ ( 𝑁 ∈ ℕ0 → { 𝑎 ∣ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) } )
61 4 60 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) } )
62 nfcv ⊢ Ⅎ 𝑢 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
63 nfcv ⊢ Ⅎ 𝑎 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
64 nfv ⊢ Ⅎ 𝑎 ∃ 𝑣 ∈ ℕ0 𝜓
65 nfcv ⊢ Ⅎ 𝑢 ℕ0
66 nfcv ⊢ Ⅎ 𝑢 𝑏
67 nfsbc1v ⊢ Ⅎ 𝑢 [ 𝑎 / 𝑢 ] 𝜓
68 66 67 nfsbcw ⊢ Ⅎ 𝑢 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓
69 65 68 nfrex ⊢ Ⅎ 𝑢 ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓
70 sbceq1a ⊢ ( 𝑢 = 𝑎 → ( 𝜓 ↔ [ 𝑎 / 𝑢 ] 𝜓 ) )
71 70 rexbidv ⊢ ( 𝑢 = 𝑎 → ( ∃ 𝑣 ∈ ℕ0 𝜓 ↔ ∃ 𝑣 ∈ ℕ0 [ 𝑎 / 𝑢 ] 𝜓 ) )
72 nfv ⊢ Ⅎ 𝑏 [ 𝑎 / 𝑢 ] 𝜓
73 nfsbc1v ⊢ Ⅎ 𝑣 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓
74 sbceq1a ⊢ ( 𝑣 = 𝑏 → ( [ 𝑎 / 𝑢 ] 𝜓 ↔ [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
75 72 73 74 cbvrexw ⊢ ( ∃ 𝑣 ∈ ℕ0 [ 𝑎 / 𝑢 ] 𝜓 ↔ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 )
76 71 75 bitrdi ⊢ ( 𝑢 = 𝑎 → ( ∃ 𝑣 ∈ ℕ0 𝜓 ↔ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 ) )
77 62 63 64 69 76 cbvrabw ⊢ { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜓 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 [ 𝑏 / 𝑣 ] [ 𝑎 / 𝑢 ] 𝜓 }
78 fveq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 ‘ 𝑀 ) = ( 𝑏 ‘ 𝑀 ) )
79 reseq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 ↾ ( 1 ... 𝑁 ) ) = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) )
80 79 sbceq1d ⊢ ( 𝑡 = 𝑏 → ( [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ↔ [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
81 78 80 sbceqbid ⊢ ( 𝑡 = 𝑏 → ( [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ↔ [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ) )
82 81 rexrab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
83 82 abbii ⊢ { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ( [ ( 𝑏 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑏 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) }
84 61 77 83 3eqtr4g ⊢ ( 𝑁 ∈ ℕ0 → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜓 } = { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } )
85 fvex ⊢ ( 𝑡 ‘ 𝑀 ) ∈ V
86 vex ⊢ 𝑡 ∈ V
87 86 resex ⊢ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ∈ V
88 2 3 sylan9bb ⊢ ( ( 𝑣 = ( 𝑡 ‘ 𝑀 ) ∧ 𝑢 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ) → ( 𝜓 ↔ 𝜑 ) )
89 85 87 88 sbc2ie ⊢ ( [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 ↔ 𝜑 )
90 89 rabbii ⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 }
91 90 rexeqi ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) )
92 91 abbii ⊢ { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ [ ( 𝑡 ‘ 𝑀 ) / 𝑣 ] [ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ] 𝜓 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } = { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) }
93 84 92 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜓 } = { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } )
94 93 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜓 } = { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } )
95 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → 𝑁 ∈ ℕ0 )
96 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
97 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
98 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
99 96 97 98 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
100 1 99 eqeltrid ⊢ ( 𝑁 ∈ ℕ0 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
101 100 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
102 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) )
103 diophrex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )
104 95 101 102 103 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )
105 94 104 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑣 ∈ ℕ0 𝜓 } ∈ ( Dioph ‘ 𝑁 ) )