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 biimtrdi ⊢ 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 biimtrid ⊢ R ⁡ X = R ⁡ Y → X ∈ U → Y ∈ U