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 e. U <-> E. x e. 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 " ( R " J ) )
5	4	eleq2i	|- ( X e. U <-> X e. ( `' R " ( 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 e. ( `' R " ( R " J ) ) <-> ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " J ) ) ) )
11	9 10	ax-mp	|- ( X e. ( `' R " ( R " J ) ) <-> ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " J ) ) )
12	6 2	mppspst	|- J C_ ( mPreSt ` T )
13		fvelimab	|- ( ( R Fn ( mPreSt ` T ) /\ J C_ ( mPreSt ` T ) ) -> ( ( R ` X ) e. ( R " J ) <-> E. x e. J ( R ` x ) = ( R ` X ) ) )
14	9 12 13	mp2an	|- ( ( R ` X ) e. ( R " J ) <-> E. x e. J ( R ` x ) = ( R ` X ) )
15	14	anbi2i	|- ( ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " J ) ) <-> ( X e. ( mPreSt ` T ) /\ E. x e. J ( R ` x ) = ( R ` X ) ) )
16	12	sseli	|- ( x e. J -> x e. ( mPreSt ` T ) )
17	6 1	msrrcl	|- ( ( R ` x ) = ( R ` X ) -> ( x e. ( mPreSt ` T ) <-> X e. ( mPreSt ` T ) ) )
18	16 17	syl5ibcom	|- ( x e. J -> ( ( R ` x ) = ( R ` X ) -> X e. ( mPreSt ` T ) ) )
19	18	rexlimiv	|- ( E. x e. J ( R ` x ) = ( R ` X ) -> X e. ( mPreSt ` T ) )
20	19	pm4.71ri	|- ( E. x e. J ( R ` x ) = ( R ` X ) <-> ( X e. ( mPreSt ` T ) /\ E. x e. J ( R ` x ) = ( R ` X ) ) )
21	15 20	bitr4i	|- ( ( X e. ( mPreSt ` T ) /\ ( R ` X ) e. ( R " J ) ) <-> E. x e. J ( R ` x ) = ( R ` X ) )
22	5 11 21	3bitri	|- ( X e. U <-> E. x e. J ( R ` x ) = ( R ` X ) )