Theorem mthmblem

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

	Ref	Expression
Hypotheses	mthmb.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mthmb.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
Assertion	mthmblem	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		mthmb.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mthmb.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
3		eqid	⊢ ( mPPSt ‘ 𝑇 ) = ( mPPSt ‘ 𝑇 )
4	1 3 2	mthmval	⊢ 𝑈 = ( ◡ 𝑅 “ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) )
5	4	eleq2i	⊢ ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∈ ( ◡ 𝑅 “ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) )
6		eqid	⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
7	6 1	msrf	⊢ 𝑅 : ( mPreSt ‘ 𝑇 ) ⟶ ( mPreSt ‘ 𝑇 )
8		ffn	⊢ ( 𝑅 : ( mPreSt ‘ 𝑇 ) ⟶ ( mPreSt ‘ 𝑇 ) → 𝑅 Fn ( mPreSt ‘ 𝑇 ) )
9	7 8	ax-mp	⊢ 𝑅 Fn ( mPreSt ‘ 𝑇 )
10		elpreima	⊢ ( 𝑅 Fn ( mPreSt ‘ 𝑇 ) → ( 𝑋 ∈ ( ◡ 𝑅 “ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) ↔ ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) ) )
11	9 10	ax-mp	⊢ ( 𝑋 ∈ ( ◡ 𝑅 “ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) ↔ ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) )
12	5 11	bitri	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) )
13		eleq1	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ↔ ( 𝑅 ‘ 𝑌 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) )
14		ffun	⊢ ( 𝑅 : ( mPreSt ‘ 𝑇 ) ⟶ ( mPreSt ‘ 𝑇 ) → Fun 𝑅 )
15	7 14	ax-mp	⊢ Fun 𝑅
16		fvelima	⊢ ( ( Fun 𝑅 ∧ ( 𝑅 ‘ 𝑌 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) → ∃ 𝑥 ∈ ( mPPSt ‘ 𝑇 ) ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑌 ) )
17	15 16	mpan	⊢ ( ( 𝑅 ‘ 𝑌 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) → ∃ 𝑥 ∈ ( mPPSt ‘ 𝑇 ) ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑌 ) )
18	1 3 2	mthmi	⊢ ( ( 𝑥 ∈ ( mPPSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑌 ) ) → 𝑌 ∈ 𝑈 )
19	18	rexlimiva	⊢ ( ∃ 𝑥 ∈ ( mPPSt ‘ 𝑇 ) ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑌 ) → 𝑌 ∈ 𝑈 )
20	17 19	syl	⊢ ( ( 𝑅 ‘ 𝑌 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) → 𝑌 ∈ 𝑈 )
21	13 20	biimtrdi	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) → 𝑌 ∈ 𝑈 ) )
22	21	adantld	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) → 𝑌 ∈ 𝑈 ) )
23	12 22	biimtrid	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈 ) )