Metamath Proof Explorer


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