Theorem fin1a2lem3

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypothesis	fin1a2lem.b	$$⊢E=\left(x\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}x\right)$$
Assertion	fin1a2lem3	$$⊢A\in \mathrm{\omega }\to E\left(A\right)=2_{𝑜}{\cdot }_{𝑜}A$$

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	$$⊢E=\left(x\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}x\right)$$
2		oveq2	$$⊢a=A\to 2_{𝑜}{\cdot }_{𝑜}a=2_{𝑜}{\cdot }_{𝑜}A$$
3		oveq2	$$⊢x=a\to 2_{𝑜}{\cdot }_{𝑜}x=2_{𝑜}{\cdot }_{𝑜}a$$
4	3	cbvmptv	$$⊢\left(x\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}x\right)=\left(a\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}a\right)$$
5	1 4	eqtri	$$⊢E=\left(a\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}a\right)$$
6		ovex	$$⊢2_{𝑜}{\cdot }_{𝑜}A\in \mathrm{V}$$
7	2 5 6	fvmpt	$$⊢A\in \mathrm{\omega }\to E\left(A\right)=2_{𝑜}{\cdot }_{𝑜}A$$