Metamath Proof Explorer

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 syl6bi ⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) → 𝑌 ∈ 𝑈 ) )
22 21 adantld ⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ ( mPPSt ‘ 𝑇 ) ) ) → 𝑌 ∈ 𝑈 ) )
23 12 22 syl5bi ⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈 ) )