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	ffvelrni	|- ( X e. P -> ( R ` X ) e. P )
5	4	a1i	|- ( ( R ` X ) = ( R ` Y ) -> ( X e. P -> ( R ` X ) e. P ) )
6	3	ffvelrni	|- ( Y e. P -> ( R ` Y ) e. P )
7		eleq1	|- ( ( R ` X ) = ( R ` Y ) -> ( ( R ` X ) e. P <-> ( R ` Y ) e. P ) )
8	6 7	syl5ibr	|- ( ( 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 ) )