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 \in U \leftrightarrow \exists x \in 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 \in U \leftrightarrow X \in 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) \to R Fn mPreSt (T)$
9	7 8	ax-mp	$⊢ R Fn mPreSt (T)$
10		elpreima	$⊢ R Fn mPreSt (T) \to (X \in R^{-1} [R [J]] \leftrightarrow (X \in mPreSt (T) \land R (X) \in R [J]))$
11	9 10	ax-mp	$⊢ X \in R^{-1} [R [J]] \leftrightarrow (X \in mPreSt (T) \land R (X) \in R [J])$
12	6 2	mppspst	$⊢ J \subseteq mPreSt (T)$
13		fvelimab	$⊢ (R Fn mPreSt (T) \land J \subseteq mPreSt (T)) \to (R (X) \in R [J] \leftrightarrow \exists x \in J R (x) = R (X))$
14	9 12 13	mp2an	$⊢ R (X) \in R [J] \leftrightarrow \exists x \in J R (x) = R (X)$
15	14	anbi2i	$⊢ (X \in mPreSt (T) \land R (X) \in R [J]) \leftrightarrow (X \in mPreSt (T) \land \exists x \in J R (x) = R (X))$
16	12	sseli	$⊢ x \in J \to x \in mPreSt (T)$
17	6 1	msrrcl	$⊢ R (x) = R (X) \to (x \in mPreSt (T) \leftrightarrow X \in mPreSt (T))$
18	16 17	syl5ibcom	$⊢ x \in J \to (R (x) = R (X) \to X \in mPreSt (T))$
19	18	rexlimiv	$⊢ \exists x \in J R (x) = R (X) \to X \in mPreSt (T)$
20	19	pm4.71ri	$⊢ \exists x \in J R (x) = R (X) \leftrightarrow (X \in mPreSt (T) \land \exists x \in J R (x) = R (X))$
21	15 20	bitr4i	$⊢ (X \in mPreSt (T) \land R (X) \in R [J]) \leftrightarrow \exists x \in J R (x) = R (X)$
22	5 11 21	3bitri	$⊢ X \in U \leftrightarrow \exists x \in J R (x) = R (X)$

Metamath Proof Explorer

Theorem elmthm

Proof