Description: Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | psr1rcl.p | ⊢ 𝑃 = ( PwSer1 ‘ 𝑅 ) | |
psr1rcl.b | ⊢ 𝐵 = ( Base ‘ 𝑃 ) | ||
psr1basf.k | ⊢ 𝐾 = ( Base ‘ 𝑅 ) | ||
Assertion | psr1basf | ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psr1rcl.p | ⊢ 𝑃 = ( PwSer1 ‘ 𝑅 ) | |
2 | psr1rcl.b | ⊢ 𝐵 = ( Base ‘ 𝑃 ) | |
3 | psr1basf.k | ⊢ 𝐾 = ( Base ‘ 𝑅 ) | |
4 | elmapi | ⊢ ( 𝐹 ∈ ( 𝐾 ↑m ( ℕ0 ↑m 1o ) ) → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ) | |
5 | 1 2 3 | psr1bas | ⊢ 𝐵 = ( 𝐾 ↑m ( ℕ0 ↑m 1o ) ) |
6 | 4 5 | eleq2s | ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ) |