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	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	msrf.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
Assertion	msrrcl	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		msrf.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
3	1 2	msrf	⊢ 𝑅 : 𝑃 ⟶ 𝑃
4	3	ffvelcdmi	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 )
5	4	a1i	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑃 → ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 ) )
6	3	ffvelcdmi	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑅 ‘ 𝑌 ) ∈ 𝑃 )
7		eleq1	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 ↔ ( 𝑅 ‘ 𝑌 ) ∈ 𝑃 ) )
8	6 7	imbitrrid	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑌 ∈ 𝑃 → ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 ) )
9	3	fdmi	⊢ dom 𝑅 = 𝑃
10		0nelxp	⊢ ¬ ∅ ∈ ( ( V × V ) × V )
11	1	mpstssv	⊢ 𝑃 ⊆ ( ( V × V ) × V )
12	11	sseli	⊢ ( ∅ ∈ 𝑃 → ∅ ∈ ( ( V × V ) × V ) )
13	10 12	mto	⊢ ¬ ∅ ∈ 𝑃
14	9 13	ndmfvrcl	⊢ ( ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 → 𝑋 ∈ 𝑃 )
15	14	adantl	⊢ ( ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 ) → 𝑋 ∈ 𝑃 )
16	7	biimpa	⊢ ( ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 ) → ( 𝑅 ‘ 𝑌 ) ∈ 𝑃 )
17	9 13	ndmfvrcl	⊢ ( ( 𝑅 ‘ 𝑌 ) ∈ 𝑃 → 𝑌 ∈ 𝑃 )
18	16 17	syl	⊢ ( ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 ) → 𝑌 ∈ 𝑃 )
19	15 18	2thd	⊢ ( ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 ) → ( 𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃 ) )
20	19	ex	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( ( 𝑅 ‘ 𝑋 ) ∈ 𝑃 → ( 𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃 ) ) )
21	5 8 20	pm5.21ndd	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃 ) )