Metamath Proof Explorer


Theorem msrrcl

Description: If X and Y have the same reduct, then one is a pre-statement iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mpstssv.p P = mPreSt T
msrf.r R = mStRed T
Assertion msrrcl R X = R Y X P Y P

Proof

Step Hyp Ref Expression
1 mpstssv.p P = mPreSt T
2 msrf.r R = mStRed T
3 1 2 msrf R : P P
4 3 ffvelrni X P R X P
5 4 a1i R X = R Y X P R X P
6 3 ffvelrni Y P R Y P
7 eleq1 R X = R Y R X P R Y P
8 6 7 syl5ibr R X = R Y Y P R X P
9 3 fdmi dom R = P
10 0nelxp ¬ V × V × V
11 1 mpstssv P V × V × V
12 11 sseli P V × V × V
13 10 12 mto ¬ P
14 9 13 ndmfvrcl R X P X P
15 14 adantl R X = R Y R X P X P
16 7 biimpa R X = R Y R X P R Y P
17 9 13 ndmfvrcl R Y P Y P
18 16 17 syl R X = R Y R X P Y P
19 15 18 2thd R X = R Y R X P X P Y P
20 19 ex R X = R Y R X P X P Y P
21 5 8 20 pm5.21ndd R X = R Y X P Y P