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	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrelbasfun.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	psrelbasfun	⊢ ( 𝑋 ∈ 𝐵 → Fun 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		psrelbasfun.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrelbasfun.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5		id	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐵 )
6	1 3 4 2 5	psrelbas	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
7	6	ffund	⊢ ( 𝑋 ∈ 𝐵 → Fun 𝑋 )