This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrelbasfun

Description: An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019)

Ref Expression
Hypotheses psrelbasfun.s ⊢ S = I mPwSer R
psrelbasfun.b ⊢ B = Base S
Assertion psrelbasfun ⊢ X ∈ B → Fun ⁡ X

Proof

Step Hyp Ref Expression
1 psrelbasfun.s ⊢ S = I mPwSer R
2 psrelbasfun.b ⊢ B = Base S
3 eqid ⊢ Base R = Base R
4 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
5 id ⊢ X ∈ B → X ∈ B
6 1 3 4 2 5 psrelbas ⊢ X ∈ B → X : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base R
7 6 ffund ⊢ X ∈ B → Fun ⁡ X