Theorem msrfo

Description: The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mstaval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mstaval.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
	msrfo.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
Assertion	msrfo	⊢ 𝑅 : 𝑃 –onto→ 𝑆

Proof

Step	Hyp	Ref	Expression
1		mstaval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mstaval.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
3		msrfo.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
4	3 1	msrf	⊢ 𝑅 : 𝑃 ⟶ 𝑃
5		ffn	⊢ ( 𝑅 : 𝑃 ⟶ 𝑃 → 𝑅 Fn 𝑃 )
6	4 5	ax-mp	⊢ 𝑅 Fn 𝑃
7		dffn4	⊢ ( 𝑅 Fn 𝑃 ↔ 𝑅 : 𝑃 –onto→ ran 𝑅 )
8	6 7	mpbi	⊢ 𝑅 : 𝑃 –onto→ ran 𝑅
9	1 2	mstaval	⊢ 𝑆 = ran 𝑅
10		foeq3	⊢ ( 𝑆 = ran 𝑅 → ( 𝑅 : 𝑃 –onto→ 𝑆 ↔ 𝑅 : 𝑃 –onto→ ran 𝑅 ) )
11	9 10	ax-mp	⊢ ( 𝑅 : 𝑃 –onto→ 𝑆 ↔ 𝑅 : 𝑃 –onto→ ran 𝑅 )
12	8 11	mpbir	⊢ 𝑅 : 𝑃 –onto→ 𝑆