Metamath Proof Explorer

Theorem elmzpcl

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

		Ref	Expression
	Assertion	elmzpcl	$⊢ V \in V \to (P \in mzPolyCld (V) \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))))$

Proof

Step	Hyp	Ref	Expression
1		mzpclval	$⊢ V \in V \to mzPolyCld (V) = \{p \in 𝒫 (ℤ^{(ℤ^{V})}) \| ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in p \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in p) \land \forall f \in p \forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p))\}$
2	1	eleq2d	$⊢ V \in V \to (P \in mzPolyCld (V) \leftrightarrow P \in \{p \in 𝒫 (ℤ^{(ℤ^{V})}) \| ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in p \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in p) \land \forall f \in p \forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p))\})$
3		eleq2	$⊢ p = P \to ((ℤ^{V}) \times \{i\} \in p \leftrightarrow (ℤ^{V}) \times \{i\} \in P)$
4	3	ralbidv	$⊢ p = P \to (\forall i \in ℤ (ℤ^{V}) \times \{i\} \in p \leftrightarrow \forall i \in ℤ (ℤ^{V}) \times \{i\} \in P)$
5		eleq2	$⊢ p = P \to ((x \in (ℤ^{V}) ⟼ x (j)) \in p \leftrightarrow (x \in (ℤ^{V}) ⟼ x (j)) \in P)$
6	5	ralbidv	$⊢ p = P \to (\forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in p \leftrightarrow \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P)$
7	4 6	anbi12d	$⊢ p = P \to ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in p \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in p) \leftrightarrow (\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P))$
8		eleq2	$⊢ p = P \to (f +_{f} g \in p \leftrightarrow f +_{f} g \in P)$
9		eleq2	$⊢ p = P \to (f \times_{f} g \in p \leftrightarrow f \times_{f} g \in P)$
10	8 9	anbi12d	$⊢ p = P \to ((f +_{f} g \in p \land f \times_{f} g \in p) \leftrightarrow (f +_{f} g \in P \land f \times_{f} g \in P))$
11	10	raleqbi1dv	$⊢ p = P \to (\forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p) \leftrightarrow \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))$
12	11	raleqbi1dv	$⊢ p = P \to (\forall f \in p \forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p) \leftrightarrow \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))$
13	7 12	anbi12d	$⊢ p = P \to (((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in p \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in p) \land \forall f \in p \forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p)) \leftrightarrow ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)))$
14	13	elrab	$⊢ P \in \{p \in 𝒫 (ℤ^{(ℤ^{V})}) \| ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in p \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in p) \land \forall f \in p \forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p))\} \leftrightarrow (P \in 𝒫 (ℤ^{(ℤ^{V})}) \land ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)))$
15		ovex	$⊢ ℤ^{(ℤ^{V})} \in V$
16	15	elpw2	$⊢ P \in 𝒫 (ℤ^{(ℤ^{V})}) \leftrightarrow P \subseteq ℤ^{(ℤ^{V})}$
17	16	anbi1i	$⊢ (P \in 𝒫 (ℤ^{(ℤ^{V})}) \land ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))) \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)))$
18	14 17	bitri	$⊢ P \in \{p \in 𝒫 (ℤ^{(ℤ^{V})}) \| ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in p \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in p) \land \forall f \in p \forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p))\} \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)))$
19	2 18	bitrdi	$⊢ V \in V \to (P \in mzPolyCld (V) \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall i \in ℤ (ℤ^{V}) \times \{i\} \in P \land \forall j \in V (x \in (ℤ^{V}) ⟼ x (j)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))))$