Theorem psr1basf

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

	Ref	Expression
Hypotheses	psr1rcl.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
	psr1rcl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	psr1basf.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion	psr1basf	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		psr1rcl.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
2		psr1rcl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		psr1basf.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		elmapi	⊢ ( 𝐹 ∈ ( 𝐾 ↑m ( ℕ0 ↑m 1o ) ) → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
5	1 2 3	psr1bas	⊢ 𝐵 = ( 𝐾 ↑m ( ℕ0 ↑m 1o ) )
6	4 5	eleq2s	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )