Metamath Proof Explorer

Theorem elmthm

Description: A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mthmval.r ⊢ R = mStRed ⁡ T
mthmval.j ⊢ J = mPPSt ⁡ T
mthmval.u ⊢ U = mThm ⁡ T
Assertion elmthm ⊢ X ∈ U ↔ ∃ x ∈ J R ⁡ x = R ⁡ X

Proof

Step Hyp Ref Expression
1 mthmval.r ⊢ R = mStRed ⁡ T
2 mthmval.j ⊢ J = mPPSt ⁡ T
3 mthmval.u ⊢ U = mThm ⁡ T
4 1 2 3 mthmval ⊢ U = R -1 R J
5 4 eleq2i ⊢ X ∈ U ↔ X ∈ R -1 R J
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 J ↔ X ∈ mPreSt ⁡ T ∧ R ⁡ X ∈ R J
11 9 10 ax-mp ⊢ X ∈ R -1 R J ↔ X ∈ mPreSt ⁡ T ∧ R ⁡ X ∈ R J
12 6 2 mppspst ⊢ J ⊆ mPreSt ⁡ T
13 fvelimab ⊢ R Fn mPreSt ⁡ T ∧ J ⊆ mPreSt ⁡ T → R ⁡ X ∈ R J ↔ ∃ x ∈ J R ⁡ x = R ⁡ X
14 9 12 13 mp2an ⊢ R ⁡ X ∈ R J ↔ ∃ x ∈ J R ⁡ x = R ⁡ X
15 14 anbi2i ⊢ X ∈ mPreSt ⁡ T ∧ R ⁡ X ∈ R J ↔ X ∈ mPreSt ⁡ T ∧ ∃ x ∈ J R ⁡ x = R ⁡ X
16 12 sseli ⊢ x ∈ J → x ∈ mPreSt ⁡ T
17 6 1 msrrcl ⊢ R ⁡ x = R ⁡ X → x ∈ mPreSt ⁡ T ↔ X ∈ mPreSt ⁡ T
18 16 17 syl5ibcom ⊢ x ∈ J → R ⁡ x = R ⁡ X → X ∈ mPreSt ⁡ T
19 18 rexlimiv ⊢ ∃ x ∈ J R ⁡ x = R ⁡ X → X ∈ mPreSt ⁡ T
20 19 pm4.71ri ⊢ ∃ x ∈ J R ⁡ x = R ⁡ X ↔ X ∈ mPreSt ⁡ T ∧ ∃ x ∈ J R ⁡ x = R ⁡ X
21 15 20 bitr4i ⊢ X ∈ mPreSt ⁡ T ∧ R ⁡ X ∈ R J ↔ ∃ x ∈ J R ⁡ x = R ⁡ X
22 5 11 21 3bitri ⊢ X ∈ U ↔ ∃ x ∈ J R ⁡ x = R ⁡ X