Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  msrfval Structured version   Visualization version   GIF version

Theorem msrfval 32304
Description: Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
msrfval.v 𝑉 = (mVars‘𝑇)
msrfval.p 𝑃 = (mPreSt‘𝑇)
msrfval.r 𝑅 = (mStRed‘𝑇)
Assertion
Ref Expression
msrfval 𝑅 = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
Distinct variable groups:   ,𝑎,𝑠,𝑧,𝑃   𝑇,𝑎,,𝑠   𝑧,𝑉
Allowed substitution hints:   𝑅(𝑧,,𝑠,𝑎)   𝑇(𝑧)   𝑉(,𝑠,𝑎)

Proof of Theorem msrfval
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 msrfval.r . 2 𝑅 = (mStRed‘𝑇)
2 fveq2 6493 . . . . . 6 (𝑡 = 𝑇 → (mPreSt‘𝑡) = (mPreSt‘𝑇))
3 msrfval.p . . . . . 6 𝑃 = (mPreSt‘𝑇)
42, 3syl6eqr 2826 . . . . 5 (𝑡 = 𝑇 → (mPreSt‘𝑡) = 𝑃)
5 fveq2 6493 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (mVars‘𝑡) = (mVars‘𝑇))
6 msrfval.v . . . . . . . . . . . . 13 𝑉 = (mVars‘𝑇)
75, 6syl6eqr 2826 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (mVars‘𝑡) = 𝑉)
87imaeq1d 5763 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((mVars‘𝑡) “ ( ∪ {𝑎})) = (𝑉 “ ( ∪ {𝑎})))
98unieqd 4716 . . . . . . . . . 10 (𝑡 = 𝑇 ((mVars‘𝑡) “ ( ∪ {𝑎})) = (𝑉 “ ( ∪ {𝑎})))
109csbeq1d 3787 . . . . . . . . 9 (𝑡 = 𝑇 ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧) = (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧))
1110ineq2d 4070 . . . . . . . 8 (𝑡 = 𝑇 → ((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)) = ((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)))
1211oteq1d 4683 . . . . . . 7 (𝑡 = 𝑇 → ⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩ = ⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
1312csbeq2dv 4250 . . . . . 6 (𝑡 = 𝑇(2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩ = (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
1413csbeq2dv 4250 . . . . 5 (𝑡 = 𝑇(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩ = (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
154, 14mpteq12dv 5006 . . . 4 (𝑡 = 𝑇 → (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
16 df-msr 32261 . . . 4 mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
1715, 16, 3mptfvmpt 6810 . . 3 (𝑇 ∈ V → (mStRed‘𝑇) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
18 mpt0 6314 . . . . 5 (𝑠 ∈ ∅ ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩) = ∅
1918eqcomi 2781 . . . 4 ∅ = (𝑠 ∈ ∅ ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
20 fvprc 6486 . . . 4 𝑇 ∈ V → (mStRed‘𝑇) = ∅)
21 fvprc 6486 . . . . . 6 𝑇 ∈ V → (mPreSt‘𝑇) = ∅)
223, 21syl5eq 2820 . . . . 5 𝑇 ∈ V → 𝑃 = ∅)
2322mpteq1d 5010 . . . 4 𝑇 ∈ V → (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩) = (𝑠 ∈ ∅ ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
2419, 20, 233eqtr4a 2834 . . 3 𝑇 ∈ V → (mStRed‘𝑇) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
2517, 24pm2.61i 177 . 2 (mStRed‘𝑇) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
261, 25eqtri 2796 1 𝑅 = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1507  wcel 2050  Vcvv 3409  csb 3780  cun 3821  cin 3822  c0 4172  {csn 4435  cotp 4443   cuni 4706  cmpt 5002   × cxp 5399  cima 5404  cfv 6182  1st c1st 7493  2nd c2nd 7494  mVarscmvrs 32236  mPreStcmpst 32240  mStRedcmsr 32241
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-ot 4444  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-msr 32261
This theorem is referenced by:  msrval  32305  msrf  32309
  Copyright terms: Public domain W3C validator