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) \to (X \in P \leftrightarrow Y \in P)$

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 \in P \to R (X) \in P$
5	4	a1i	$⊢ R (X) = R (Y) \to (X \in P \to R (X) \in P)$
6	3	ffvelcdmi	$⊢ Y \in P \to R (Y) \in P$
7		eleq1	$⊢ R (X) = R (Y) \to (R (X) \in P \leftrightarrow R (Y) \in P)$
8	6 7	imbitrrid	$⊢ R (X) = R (Y) \to (Y \in P \to R (X) \in P)$
9	3	fdmi	$⊢ dom R = P$
10		0nelxp	$⊢ \neg \emptyset \in ((V \times V) \times V)$
11	1	mpstssv	$⊢ P \subseteq (V \times V) \times V$
12	11	sseli	$⊢ \emptyset \in P \to \emptyset \in ((V \times V) \times V)$
13	10 12	mto	$⊢ \neg \emptyset \in P$
14	9 13	ndmfvrcl	$⊢ R (X) \in P \to X \in P$
15	14	adantl	$⊢ (R (X) = R (Y) \land R (X) \in P) \to X \in P$
16	7	biimpa	$⊢ (R (X) = R (Y) \land R (X) \in P) \to R (Y) \in P$
17	9 13	ndmfvrcl	$⊢ R (Y) \in P \to Y \in P$
18	16 17	syl	$⊢ (R (X) = R (Y) \land R (X) \in P) \to Y \in P$
19	15 18	2thd	$⊢ (R (X) = R (Y) \land R (X) \in P) \to (X \in P \leftrightarrow Y \in P)$
20	19	ex	$⊢ R (X) = R (Y) \to (R (X) \in P \to (X \in P \leftrightarrow Y \in P))$
21	5 8 20	pm5.21ndd	$⊢ R (X) = R (Y) \to (X \in P \leftrightarrow Y \in P)$

Metamath Proof Explorer