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=\mathrm{mStRed}\left(T\right)$$
	mstaval.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
	msrfo.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
Assertion	msrfo	$$⊢R:P\underset{onto}{⟶}S$$

Proof

Step	Hyp	Ref	Expression
1		mstaval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
2		mstaval.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
3		msrfo.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
4	3 1	msrf	$$⊢R:P⟶P$$
5		ffn	$$⊢R:P⟶P\to RFnP$$
6	4 5	ax-mp	$$⊢RFnP$$
7		dffn4	$$⊢RFnP\leftrightarrow R:P\underset{onto}{⟶}\mathrm{ran}R$$
8	6 7	mpbi	$$⊢R:P\underset{onto}{⟶}\mathrm{ran}R$$
9	1 2	mstaval	$$⊢S=\mathrm{ran}R$$
10		foeq3	$$⊢S=\mathrm{ran}R\to \left(R:P\underset{onto}{⟶}S\leftrightarrow R:P\underset{onto}{⟶}\mathrm{ran}R\right)$$
11	9 10	ax-mp	$$⊢R:P\underset{onto}{⟶}S\leftrightarrow R:P\underset{onto}{⟶}\mathrm{ran}R$$
12	8 11	mpbir	$$⊢R:P\underset{onto}{⟶}S$$