This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ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 ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ 𝐾 )