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	⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → 𝐵 ∈ V )
2		fveq2	⊢ ( 𝑑 = 𝐵 → ( mzPoly ‘ 𝑑 ) = ( mzPoly ‘ 𝐵 ) )
3	2	eleq2d	⊢ ( 𝑑 = 𝐵 → ( 𝐴 ∈ ( mzPoly ‘ 𝑑 ) ↔ 𝐴 ∈ ( mzPoly ‘ 𝐵 ) ) )
4		sseq2	⊢ ( 𝑑 = 𝐵 → ( 𝑎 ⊆ 𝑑 ↔ 𝑎 ⊆ 𝐵 ) )
5		oveq2	⊢ ( 𝑑 = 𝐵 → ( ℤ ↑m 𝑑 ) = ( ℤ ↑m 𝐵 ) )
6	5	mpteq1d	⊢ ( 𝑑 = 𝐵 → ( 𝑐 ∈ ( ℤ ↑m 𝑑 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) )
7	6	eqeq2d	⊢ ( 𝑑 = 𝐵 → ( 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝑑 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ↔ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )
8	4 7	anbi12d	⊢ ( 𝑑 = 𝐵 → ( ( 𝑎 ⊆ 𝑑 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝑑 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) ) )
9	8	2rexbidv	⊢ ( 𝑑 = 𝐵 → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝑑 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝑑 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) ) )
10	3 9	imbi12d	⊢ ( 𝑑 = 𝐵 → ( ( 𝐴 ∈ ( mzPoly ‘ 𝑑 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝑑 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝑑 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) ) ↔ ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) ) ) )
11		vex	⊢ 𝑑 ∈ V
12	11	mzpcompact2lem	⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝑑 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝑑 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝑑 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )
13	10 12	vtoclg	⊢ ( 𝐵 ∈ V → ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) ) )
14	1 13	mpcom	⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )