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 𝑅 ) ‘ ∅ )