Metamath Proof Explorer


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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
psrbas.b 𝐵 = ( Base ‘ 𝑆 )
psrelbas.x ( 𝜑𝑋𝐵 )
Assertion psrelbas ( 𝜑𝑋 : 𝐷𝐾 )

Proof

Step Hyp Ref Expression
1 psrbas.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrbas.k 𝐾 = ( Base ‘ 𝑅 )
3 psrbas.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 ( ℕ0m 𝐼 ) ∈ V
14 3 13 rabex2 𝐷 ∈ V
15 12 14 elmap ( 𝑋 ∈ ( 𝐾m 𝐷 ) ↔ 𝑋 : 𝐷𝐾 )
16 11 15 sylib ( 𝜑𝑋 : 𝐷𝐾 )