Theorem msrfo

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

	Ref	Expression
Hypotheses	mstaval.r	|- R = ( mStRed ` T )
	mstaval.s	|- S = ( mStat ` T )
	msrfo.p	|- P = ( mPreSt ` T )
Assertion	msrfo	|- R : P -onto-> S

Proof

Step	Hyp	Ref	Expression
1		mstaval.r	|- R = ( mStRed ` T )
2		mstaval.s	|- S = ( mStat ` T )
3		msrfo.p	|- P = ( mPreSt ` T )
4	3 1	msrf	|- R : P --> P
5		ffn	|- ( R : P --> P -> R Fn P )
6	4 5	ax-mp	|- R Fn P
7		dffn4	|- ( R Fn P <-> R : P -onto-> ran R )
8	6 7	mpbi	|- R : P -onto-> ran R
9	1 2	mstaval	|- S = ran R
10		foeq3	|- ( S = ran R -> ( R : P -onto-> S <-> R : P -onto-> ran R ) )
11	9 10	ax-mp	|- ( R : P -onto-> S <-> R : P -onto-> ran R )
12	8 11	mpbir	|- R : P -onto-> S