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

Metamath Proof Explorer

Theorem psr1basf

Description: Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015)

Step	Hyp	Ref	Expression
1		psr1rcl.p	$⊢ P = {PwSer}_{1} (R)$
2		psr1rcl.b	$⊢ B = {Base}_{P}$
3		psr1basf.k	$⊢ K = {Base}_{R}$
4		elmapi	$⊢ F \in (K^{({ℕ_{0}}^{1_{𝑜}})}) \to F : {ℕ_{0}}^{1_{𝑜}} ⟶ K$
5	1 2 3	psr1bas	$⊢ B = K^{({ℕ_{0}}^{1_{𝑜}})}$
6	4 5	eleq2s	$⊢ F \in B \to F : {ℕ_{0}}^{1_{𝑜}} ⟶ K$