Metamath Proof Explorer


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 ( 𝐹𝐵𝐹 : ( ℕ0m 1o ) ⟶ 𝐾 )

Proof

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