Metamath Proof Explorer

Theorem eldioph3

Description: Inference version of eldioph3b with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion eldioph3 ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ℕ ) ) → 𝑁 ∈ ℕ0 )
2 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ℕ ) ) → 𝑃 ∈ ( mzPoly ‘ ℕ ) )
3 eqidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } )
4 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑏 ) = ( 𝑃 ‘ 𝑏 ) )
5 4 eqeq1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 𝑏 ) = 0 ↔ ( 𝑃 ‘ 𝑏 ) = 0 ) )
6 5 anbi2d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑏 ) = 0 ) ↔ ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ) )
7 6 rexbidv ⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑏 ) = 0 ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ) )
8 7 abbidv ⊢ ( 𝑝 = 𝑃 → { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑏 ) = 0 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) } )
9 eqeq1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
10 9 anbi1d ⊢ ( 𝑎 = 𝑡 → ( ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ↔ ( 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ) )
11 10 rexbidv ⊢ ( 𝑎 = 𝑡 → ( ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ) )
12 reseq1 ⊢ ( 𝑏 = 𝑢 → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
13 12 eqeq2d ⊢ ( 𝑏 = 𝑢 → ( 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ) )
14 fveqeq2 ⊢ ( 𝑏 = 𝑢 → ( ( 𝑃 ‘ 𝑏 ) = 0 ↔ ( 𝑃 ‘ 𝑢 ) = 0 ) )
15 13 14 anbi12d ⊢ ( 𝑏 = 𝑢 → ( ( 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ↔ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) ) )
16 15 cbvrexvw ⊢ ( ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) )
17 11 16 bitrdi ⊢ ( 𝑎 = 𝑡 → ( ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) ) )
18 17 cbvabv ⊢ { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑏 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) }
19 8 18 eqtrdi ⊢ ( 𝑝 = 𝑃 → { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑏 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } )
20 19 rspceeqv ⊢ ( ( 𝑃 ∈ ( mzPoly ‘ ℕ ) ∧ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ) → ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑏 ) = 0 ) } )
21 2 3 20 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ℕ ) ) → ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑏 ) = 0 ) } )
22 eldioph3b ⊢ ( { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ℕ ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑏 ) = 0 ) } ) )
23 1 21 22 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ℕ ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )