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 ⊢ S = I mPwSer R
psrbas.k ⊢ K = Base R
psrbas.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
psrbas.b ⊢ B = Base S
psrelbas.x ⊢ φ → X ∈ B
Assertion psrelbas ⊢ φ → X : D ⟶ K

Proof

Step Hyp Ref Expression
1 psrbas.s ⊢ S = I mPwSer R
2 psrbas.k ⊢ K = Base R
3 psrbas.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
4 psrbas.b ⊢ B = Base S
5 psrelbas.x ⊢ φ → X ∈ B
6 reldmpsr ⊢ Rel ⁡ dom ⁡ mPwSer
7 6 1 4 elbasov ⊢ X ∈ B → I ∈ V ∧ R ∈ V
8 5 7 syl ⊢ φ → I ∈ V ∧ R ∈ V
9 8 simpld ⊢ φ → I ∈ V
10 1 2 3 4 9 psrbas ⊢ φ → B = K D
11 5 10 eleqtrd ⊢ φ → X ∈ K D
12 2 fvexi ⊢ K ∈ V
13 ovex ⊢ ℕ 0 I ∈ V
14 3 13 rabex2 ⊢ D ∈ V
15 12 14 elmap ⊢ X ∈ K D ↔ X : D ⟶ K
16 11 15 sylib ⊢ φ → X : D ⟶ K