Theorem psrelbas

Description: An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Hypotheses	psrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrbas.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	psrbas.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psrbas.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psrelbas.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	psrelbas	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		psrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrbas.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		psrbas.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
4		psrbas.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		psrelbas.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		reldmpsr	⊢ Rel dom mPwSer
7	6 1 4	elbasov	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
8	5 7	syl	⊢ ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
9	8	simpld	⊢ ( 𝜑 → 𝐼 ∈ V )
10	1 2 3 4 9	psrbas	⊢ ( 𝜑 → 𝐵 = ( 𝐾 ↑m 𝐷 ) )
11	5 10	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐾 ↑m 𝐷 ) )
12	2	fvexi	⊢ 𝐾 ∈ V
13		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
14	3 13	rabex2	⊢ 𝐷 ∈ V
15	12 14	elmap	⊢ ( 𝑋 ∈ ( 𝐾 ↑m 𝐷 ) ↔ 𝑋 : 𝐷 ⟶ 𝐾 )
16	11 15	sylib	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ 𝐾 )