Theorem mthmblem

Description: Lemma for mthmb . (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mthmb.r	|- R = ( mStRed ` T )
	mthmb.u	|- U = ( mThm ` T )
Assertion	mthmblem	|- ( ( R ` X ) = ( R ` Y ) -> ( X e. U -> Y e. U ) )

Proof

Step	Hyp	Ref	Expression
1		mthmb.r	|- R = ( mStRed ` T )
2		mthmb.u	|- U = ( mThm ` T )
3		eqid	|- ( mPPSt ` T ) = ( mPPSt ` T )
4	1 3 2	mthmval	|- U = ( `' R " ( R " ( mPPSt ` T ) ) )
5	4	eleq2i	|- ( X e. U <-> X e. ( `' R " ( R " ( mPPSt ` T ) ) ) )
6		eqid	|- ( mPreSt ` T ) = ( mPreSt ` T )
7	6 1	msrf	|- R : ( mPreSt ` T ) --> ( mPreSt ` T )
8		ffn	|- ( R : ( mPreSt ` T ) --> ( mPreSt ` T ) -> R Fn ( mPreSt ` T ) )
9	7 8	ax-mp	|- R Fn ( mPreSt ` T )
10		elpreima	|- ( R Fn ( mPreSt ` T ) -> ( X e. ( `' R " ( R " ( mPPSt ` T ) ) ) <-> ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " ( mPPSt ` T ) ) ) ) )
11	9 10	ax-mp	|- ( X e. ( `' R " ( R " ( mPPSt ` T ) ) ) <-> ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " ( mPPSt ` T ) ) ) )
12	5 11	bitri	|- ( X e. U <-> ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " ( mPPSt ` T ) ) ) )
13		eleq1	|- ( ( R ` X ) = ( R ` Y ) -> ( ( R ` X ) e. ( R " ( mPPSt ` T ) ) <-> ( R ` Y ) e. ( R " ( mPPSt ` T ) ) ) )
14		ffun	|- ( R : ( mPreSt ` T ) --> ( mPreSt ` T ) -> Fun R )
15	7 14	ax-mp	|- Fun R
16		fvelima	|- ( ( Fun R /\ ( R ` Y ) e. ( R " ( mPPSt ` T ) ) ) -> E. x e. ( mPPSt ` T ) ( R ` x ) = ( R ` Y ) )
17	15 16	mpan	|- ( ( R ` Y ) e. ( R " ( mPPSt ` T ) ) -> E. x e. ( mPPSt ` T ) ( R ` x ) = ( R ` Y ) )
18	1 3 2	mthmi	|- ( ( x e. ( mPPSt ` T ) /\ ( R ` x ) = ( R ` Y ) ) -> Y e. U )
19	18	rexlimiva	|- ( E. x e. ( mPPSt ` T ) ( R ` x ) = ( R ` Y ) -> Y e. U )
20	17 19	syl	|- ( ( R ` Y ) e. ( R " ( mPPSt ` T ) ) -> Y e. U )
21	13 20	syl6bi	|- ( ( R ` X ) = ( R ` Y ) -> ( ( R ` X ) e. ( R " ( mPPSt ` T ) ) -> Y e. U ) )
22	21	adantld	|- ( ( R ` X ) = ( R ` Y ) -> ( ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " ( mPPSt ` T ) ) ) -> Y e. U ) )
23	12 22	syl5bi	|- ( ( R ` X ) = ( R ` Y ) -> ( X e. U -> Y e. U ) )