Metamath Proof Explorer

Theorem mthmval

Description: A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. Unlike the difference between pre-statement and statement, this application of the reduct is not necessarily trivial: there are theorems that are not themselves provable but are provable once enough "dummy variables" are introduced. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mthmval.r ⊢ 𝑅 = ( mStRed ‘ 𝑇 )
mthmval.j ⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
mthmval.u ⊢ 𝑈 = ( mThm ‘ 𝑇 )
Assertion mthmval 𝑈 = ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 mthmval.r ⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2 mthmval.j ⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3 mthmval.u ⊢ 𝑈 = ( mThm ‘ 𝑇 )
4 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mStRed ‘ 𝑡 ) = ( mStRed ‘ 𝑇 ) )
5 4 1 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mStRed ‘ 𝑡 ) = 𝑅 )
6 5 cnveqd ⊢ ( 𝑡 = 𝑇 → ◡ ( mStRed ‘ 𝑡 ) = ◡ 𝑅 )
7 fveq2 ⊢ ( 𝑡 = 𝑇 → ( mPPSt ‘ 𝑡 ) = ( mPPSt ‘ 𝑇 ) )
8 7 2 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( mPPSt ‘ 𝑡 ) = 𝐽 )
9 5 8 imaeq12d ⊢ ( 𝑡 = 𝑇 → ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) = ( 𝑅 “ 𝐽 ) )
10 6 9 imaeq12d ⊢ ( 𝑡 = 𝑇 → ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) ) = ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) ) )
11 df-mthm ⊢ mThm = ( 𝑡 ∈ V ↦ ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) ) )
12 fvex ⊢ ( mStRed ‘ 𝑡 ) ∈ V
13 12 cnvex ⊢ ◡ ( mStRed ‘ 𝑡 ) ∈ V
14 imaexg ⊢ ( ◡ ( mStRed ‘ 𝑡 ) ∈ V → ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) ) ∈ V )
15 13 14 ax-mp ⊢ ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) ) ∈ V
16 10 11 15 fvmpt3i ⊢ ( 𝑇 ∈ V → ( mThm ‘ 𝑇 ) = ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) ) )
17 0ima ⊢ ( ∅ “ ( 𝑅 “ 𝐽 ) ) = ∅
18 17 eqcomi ⊢ ∅ = ( ∅ “ ( 𝑅 “ 𝐽 ) )
19 fvprc ⊢ ( ¬ 𝑇 ∈ V → ( mThm ‘ 𝑇 ) = ∅ )
20 fvprc ⊢ ( ¬ 𝑇 ∈ V → ( mStRed ‘ 𝑇 ) = ∅ )
21 1 20 syl5eq ⊢ ( ¬ 𝑇 ∈ V → 𝑅 = ∅ )
22 21 cnveqd ⊢ ( ¬ 𝑇 ∈ V → ◡ 𝑅 = ◡ ∅ )
23 cnv0 ⊢ ◡ ∅ = ∅
24 22 23 eqtrdi ⊢ ( ¬ 𝑇 ∈ V → ◡ 𝑅 = ∅ )
25 24 imaeq1d ⊢ ( ¬ 𝑇 ∈ V → ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) ) = ( ∅ “ ( 𝑅 “ 𝐽 ) ) )
26 18 19 25 3eqtr4a ⊢ ( ¬ 𝑇 ∈ V → ( mThm ‘ 𝑇 ) = ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) ) )
27 16 26 pm2.61i ⊢ ( mThm ‘ 𝑇 ) = ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) )
28 3 27 eqtri ⊢ 𝑈 = ( ◡ 𝑅 “ ( 𝑅 “ 𝐽 ) )