Theorem mzpclval

Description: Substitution lemma for mzPolyCld . (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	mzpclval	⊢ ( 𝑉 ∈ V → ( mzPolyCld ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑣 = 𝑉 → ( ℤ ↑m 𝑣 ) = ( ℤ ↑m 𝑉 ) )
2	1	oveq2d	⊢ ( 𝑣 = 𝑉 → ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) = ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
3	2	pweqd	⊢ ( 𝑣 = 𝑉 → 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) = 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
4	1	xpeq1d	⊢ ( 𝑣 = 𝑉 → ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) = ( ( ℤ ↑m 𝑉 ) × { 𝑎 } ) )
5	4	eleq1d	⊢ ( 𝑣 = 𝑉 → ( ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) ∈ 𝑝 ↔ ( ( ℤ ↑m 𝑉 ) × { 𝑎 } ) ∈ 𝑝 ) )
6	5	ralbidv	⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) ∈ 𝑝 ↔ ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑎 } ) ∈ 𝑝 ) )
7		sneq	⊢ ( 𝑎 = 𝑖 → { 𝑎 } = { 𝑖 } )
8	7	xpeq2d	⊢ ( 𝑎 = 𝑖 → ( ( ℤ ↑m 𝑉 ) × { 𝑎 } ) = ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) )
9	8	eleq1d	⊢ ( 𝑎 = 𝑖 → ( ( ( ℤ ↑m 𝑉 ) × { 𝑎 } ) ∈ 𝑝 ↔ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ) )
10	9	cbvralvw	⊢ ( ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑎 } ) ∈ 𝑝 ↔ ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 )
11	6 10	bitrdi	⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) ∈ 𝑝 ↔ ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ) )
12	1	mpteq1d	⊢ ( 𝑣 = 𝑉 → ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) = ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) )
13	12	eleq1d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ↔ ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ) )
14	13	raleqbi1dv	⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑏 ∈ 𝑣 ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ↔ ∀ 𝑏 ∈ 𝑉 ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ) )
15		fveq2	⊢ ( 𝑏 = 𝑗 → ( 𝑐 ‘ 𝑏 ) = ( 𝑐 ‘ 𝑗 ) )
16	15	mpteq2dv	⊢ ( 𝑏 = 𝑗 → ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) = ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑗 ) ) )
17	16	eleq1d	⊢ ( 𝑏 = 𝑗 → ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ↔ ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑗 ) ) ∈ 𝑝 ) )
18		fveq1	⊢ ( 𝑐 = 𝑥 → ( 𝑐 ‘ 𝑗 ) = ( 𝑥 ‘ 𝑗 ) )
19	18	cbvmptv	⊢ ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑗 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) )
20	19	eleq1i	⊢ ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑗 ) ) ∈ 𝑝 ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 )
21	17 20	bitrdi	⊢ ( 𝑏 = 𝑗 → ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) )
22	21	cbvralvw	⊢ ( ∀ 𝑏 ∈ 𝑉 ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ↔ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 )
23	14 22	bitrdi	⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑏 ∈ 𝑣 ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ↔ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) )
24	11 23	anbi12d	⊢ ( 𝑣 = 𝑉 → ( ( ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) ∈ 𝑝 ∧ ∀ 𝑏 ∈ 𝑣 ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ) ↔ ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ) )
25	24	anbi1d	⊢ ( 𝑣 = 𝑉 → ( ( ( ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) ∈ 𝑝 ∧ ∀ 𝑏 ∈ 𝑣 ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) ↔ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) ) )
26	3 25	rabeqbidv	⊢ ( 𝑣 = 𝑉 → { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∣ ( ( ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) ∈ 𝑝 ∧ ∀ 𝑏 ∈ 𝑣 ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } = { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )
27		df-mzpcl	⊢ mzPolyCld = ( 𝑣 ∈ V ↦ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∣ ( ( ∀ 𝑎 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑎 } ) ∈ 𝑝 ∧ ∀ 𝑏 ∈ 𝑣 ( 𝑐 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )
28		ovex	⊢ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ V
29	28	pwex	⊢ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ V
30	29	rabex	⊢ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } ∈ V
31	26 27 30	fvmpt	⊢ ( 𝑉 ∈ V → ( mzPolyCld ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )