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 e. P <-> Y e. 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 ffvelcdmi 
 |-  ( X e. P -> ( R ` X ) e. P )
5 4 a1i 
 |-  ( ( R ` X ) = ( R ` Y ) -> ( X e. P -> ( R ` X ) e. P ) )
6 3 ffvelcdmi 
 |-  ( Y e. P -> ( R ` Y ) e. P )
7 eleq1 
 |-  ( ( R ` X ) = ( R ` Y ) -> ( ( R ` X ) e. P <-> ( R ` Y ) e. P ) )
8 6 7 imbitrrid 
 |-  ( ( R ` X ) = ( R ` Y ) -> ( Y e. P -> ( R ` X ) e. P ) )
9 3 fdmi 
 |-  dom R = P
10 0nelxp 
 |-  -. (/) e. ( ( _V X. _V ) X. _V )
11 1 mpstssv 
 |-  P C_ ( ( _V X. _V ) X. _V )
12 11 sseli 
 |-  ( (/) e. P -> (/) e. ( ( _V X. _V ) X. _V ) )
13 10 12 mto 
 |-  -. (/) e. P
14 9 13 ndmfvrcl 
 |-  ( ( R ` X ) e. P -> X e. P )
15 14 adantl 
 |-  ( ( ( R ` X ) = ( R ` Y ) /\ ( R ` X ) e. P ) -> X e. P )
16 7 biimpa 
 |-  ( ( ( R ` X ) = ( R ` Y ) /\ ( R ` X ) e. P ) -> ( R ` Y ) e. P )
17 9 13 ndmfvrcl 
 |-  ( ( R ` Y ) e. P -> Y e. P )
18 16 17 syl 
 |-  ( ( ( R ` X ) = ( R ` Y ) /\ ( R ` X ) e. P ) -> Y e. P )
19 15 18 2thd 
 |-  ( ( ( R ` X ) = ( R ` Y ) /\ ( R ` X ) e. P ) -> ( X e. P <-> Y e. P ) )
20 19 ex 
 |-  ( ( R ` X ) = ( R ` Y ) -> ( ( R ` X ) e. P -> ( X e. P <-> Y e. P ) ) )
21 5 8 20 pm5.21ndd 
 |-  ( ( R ` X ) = ( R ` Y ) -> ( X e. P <-> Y e. P ) )