Metamath Proof Explorer


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 U Y 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 -1 R mPPSt T
5 4 eleq2i X U X R -1 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 R -1 R mPPSt T X mPreSt T R X R mPPSt T
11 9 10 ax-mp X R -1 R mPPSt T X mPreSt T R X R mPPSt T
12 5 11 bitri X U X mPreSt T R X R mPPSt T
13 eleq1 R X = R Y R X R mPPSt T R Y 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 R mPPSt T x mPPSt T R x = R Y
17 15 16 mpan R Y R mPPSt T x mPPSt T R x = R Y
18 1 3 2 mthmi x mPPSt T R x = R Y Y U
19 18 rexlimiva x mPPSt T R x = R Y Y U
20 17 19 syl R Y R mPPSt T Y U
21 13 20 syl6bi R X = R Y R X R mPPSt T Y U
22 21 adantld R X = R Y X mPreSt T R X R mPPSt T Y U
23 12 22 syl5bi R X = R Y X U Y U