Metamath Proof Explorer

Theorem fin1a2lem3

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

Ref Expression
Hypothesis fin1a2lem.b ⊢ E = x ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 x
Assertion fin1a2lem3 ⊢ A ∈ ω → E ⁡ A = 2 𝑜 ⋅ 𝑜 A

Proof

Step Hyp Ref Expression
1 fin1a2lem.b ⊢ E = x ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 x
2 oveq2 ⊢ a = A → 2 𝑜 ⋅ 𝑜 a = 2 𝑜 ⋅ 𝑜 A
3 oveq2 ⊢ x = a → 2 𝑜 ⋅ 𝑜 x = 2 𝑜 ⋅ 𝑜 a
4 3 cbvmptv ⊢ x ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 x = a ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 a
5 1 4 eqtri ⊢ E = a ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 a
6 ovex ⊢ 2 𝑜 ⋅ 𝑜 A ∈ V
7 2 5 6 fvmpt ⊢ A ∈ ω → E ⁡ A = 2 𝑜 ⋅ 𝑜 A