# Metamath Proof Explorer

## Theorem psr1val

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

Ref Expression
Hypothesis psr1val.1 𝑆 = ( PwSer1𝑅 )
Assertion psr1val 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )

### Proof

Step Hyp Ref Expression
1 psr1val.1 𝑆 = ( PwSer1𝑅 )
2 oveq2 ( 𝑟 = 𝑅 → ( 1o ordPwSer 𝑟 ) = ( 1o ordPwSer 𝑅 ) )
3 2 fveq1d ( 𝑟 = 𝑅 → ( ( 1o ordPwSer 𝑟 ) ‘ ∅ ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) )
4 df-psr1 PwSer1 = ( 𝑟 ∈ V ↦ ( ( 1o ordPwSer 𝑟 ) ‘ ∅ ) )
5 fvex ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) ∈ V
6 3 4 5 fvmpt ( 𝑅 ∈ V → ( PwSer1𝑅 ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) )
7 0fv ( ∅ ‘ ∅ ) = ∅
8 7 eqcomi ∅ = ( ∅ ‘ ∅ )
9 fvprc ( ¬ 𝑅 ∈ V → ( PwSer1𝑅 ) = ∅ )
10 reldmopsr Rel dom ordPwSer
11 10 ovprc2 ( ¬ 𝑅 ∈ V → ( 1o ordPwSer 𝑅 ) = ∅ )
12 11 fveq1d ( ¬ 𝑅 ∈ V → ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) = ( ∅ ‘ ∅ ) )
13 8 9 12 3eqtr4a ( ¬ 𝑅 ∈ V → ( PwSer1𝑅 ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) )
14 6 13 pm2.61i ( PwSer1𝑅 ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
15 1 14 eqtri 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )