Metamath Proof Explorer


Theorem psr1bas

Description: The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses psr1val.1 S = PwSer 1 R
psr1bas2.b B = Base S
psr1bas.k K = Base R
Assertion psr1bas B = K 0 1 𝑜

Proof

Step Hyp Ref Expression
1 psr1val.1 S = PwSer 1 R
2 psr1bas2.b B = Base S
3 psr1bas.k K = Base R
4 eqid 1 𝑜 mPwSer R = 1 𝑜 mPwSer R
5 psr1baslem 0 1 𝑜 = f 0 1 𝑜 | f -1 Fin
6 1 2 4 psr1bas2 B = Base 1 𝑜 mPwSer R
7 1on 1 𝑜 On
8 7 a1i 1 𝑜 On
9 4 3 5 6 8 psrbas B = K 0 1 𝑜
10 9 mptru B = K 0 1 𝑜