Metamath Proof Explorer

Theorem mzpcompact2

Description: Polynomials are finitary objects and can only reference a finite number of variables, even if the index set is infinite. Thus, every polynomial can be expressed as a (uniquely minimal, although we do not prove that) polynomial on a finite number of variables, which is then extended by adding an arbitrary set of ignored variables. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion mzpcompact2 ⊢ A ∈ mzPoly ⁡ B → ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ B ∧ A = c ∈ ℤ B ⟼ b ⁡ c ↾ a

Proof

Step Hyp Ref Expression
1 elfvex ⊢ A ∈ mzPoly ⁡ B → B ∈ V
2 fveq2 ⊢ d = B → mzPoly ⁡ d = mzPoly ⁡ B
3 2 eleq2d ⊢ d = B → A ∈ mzPoly ⁡ d ↔ A ∈ mzPoly ⁡ B
4 sseq2 ⊢ d = B → a ⊆ d ↔ a ⊆ B
5 oveq2 ⊢ d = B → ℤ d = ℤ B
6 5 mpteq1d ⊢ d = B → c ∈ ℤ d ⟼ b ⁡ c ↾ a = c ∈ ℤ B ⟼ b ⁡ c ↾ a
7 6 eqeq2d ⊢ d = B → A = c ∈ ℤ d ⟼ b ⁡ c ↾ a ↔ A = c ∈ ℤ B ⟼ b ⁡ c ↾ a
8 4 7 anbi12d ⊢ d = B → a ⊆ d ∧ A = c ∈ ℤ d ⟼ b ⁡ c ↾ a ↔ a ⊆ B ∧ A = c ∈ ℤ B ⟼ b ⁡ c ↾ a
9 8 2rexbidv ⊢ d = B → ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ d ∧ A = c ∈ ℤ d ⟼ b ⁡ c ↾ a ↔ ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ B ∧ A = c ∈ ℤ B ⟼ b ⁡ c ↾ a
10 3 9 imbi12d ⊢ d = B → A ∈ mzPoly ⁡ d → ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ d ∧ A = c ∈ ℤ d ⟼ b ⁡ c ↾ a ↔ A ∈ mzPoly ⁡ B → ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ B ∧ A = c ∈ ℤ B ⟼ b ⁡ c ↾ a
11 vex ⊢ d ∈ V
12 11 mzpcompact2lem ⊢ A ∈ mzPoly ⁡ d → ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ d ∧ A = c ∈ ℤ d ⟼ b ⁡ c ↾ a
13 10 12 vtoclg ⊢ B ∈ V → A ∈ mzPoly ⁡ B → ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ B ∧ A = c ∈ ℤ B ⟼ b ⁡ c ↾ a
14 1 13 mpcom ⊢ A ∈ mzPoly ⁡ B → ∃ a ∈ Fin ∃ b ∈ mzPoly ⁡ a a ⊆ B ∧ A = c ∈ ℤ B ⟼ b ⁡ c ↾ a