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	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mthmval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
	mthmval.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
Assertion	elmthm	⊢ ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		mthmval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mthmval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3		mthmval.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
4	1 2 3	mthmval	⊢ 𝑈 = ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) )
5	4	eleq2i	⊢ ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) ) )
6		eqid	⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
7	6 1	msrf	⊢ 𝑅 : ( mPreSt ‘ 𝑇 ) ⟶ ( mPreSt ‘ 𝑇 )
8		ffn	⊢ ( 𝑅 : ( mPreSt ‘ 𝑇 ) ⟶ ( mPreSt ‘ 𝑇 ) → 𝑅 Fn ( mPreSt ‘ 𝑇 ) )
9	7 8	ax-mp	⊢ 𝑅 Fn ( mPreSt ‘ 𝑇 )
10		elpreima	⊢ ( 𝑅 Fn ( mPreSt ‘ 𝑇 ) → ( 𝑋 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) ) ↔ ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ 𝐽 ) ) ) )
11	9 10	ax-mp	⊢ ( 𝑋 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) ) ↔ ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ 𝐽 ) ) )
12	6 2	mppspst	⊢ 𝐽 ⊆ ( mPreSt ‘ 𝑇 )
13		fvelimab	⊢ ( ( 𝑅 Fn ( mPreSt ‘ 𝑇 ) ∧ 𝐽 ⊆ ( mPreSt ‘ 𝑇 ) ) → ( ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ 𝐽 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) ) )
14	9 12 13	mp2an	⊢ ( ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ 𝐽 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) )
15	14	anbi2i	⊢ ( ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ 𝐽 ) ) ↔ ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) ) )
16	12	sseli	⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ∈ ( mPreSt ‘ 𝑇 ) )
17	6 1	msrrcl	⊢ ( ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) → ( 𝑥 ∈ ( mPreSt ‘ 𝑇 ) ↔ 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ) )
18	16 17	syl5ibcom	⊢ ( 𝑥 ∈ 𝐽 → ( ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) → 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ) )
19	18	rexlimiv	⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) → 𝑋 ∈ ( mPreSt ‘ 𝑇 ) )
20	19	pm4.71ri	⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) ↔ ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) ) )
21	15 20	bitr4i	⊢ ( ( 𝑋 ∈ ( mPreSt ‘ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ∈ ( 𝑅 “ 𝐽 ) ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) )
22	5 11 21	3bitri	⊢ ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) )