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 31765
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 6330 . . . . . 6 (𝑡 = 𝑇 → (mPreSt‘𝑡) = (mPreSt‘𝑇))
3 msrfval.p . . . . . 6 𝑃 = (mPreSt‘𝑇)
42, 3syl6eqr 2823 . . . . 5 (𝑡 = 𝑇 → (mPreSt‘𝑡) = 𝑃)
5 fveq2 6330 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (mVars‘𝑡) = (mVars‘𝑇))
6 msrfval.v . . . . . . . . . . . . 13 𝑉 = (mVars‘𝑇)
75, 6syl6eqr 2823 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (mVars‘𝑡) = 𝑉)
87imaeq1d 5604 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((mVars‘𝑡) “ ( ∪ {𝑎})) = (𝑉 “ ( ∪ {𝑎})))
98unieqd 4584 . . . . . . . . . 10 (𝑡 = 𝑇 ((mVars‘𝑡) “ ( ∪ {𝑎})) = (𝑉 “ ( ∪ {𝑎})))
109csbeq1d 3689 . . . . . . . . 9 (𝑡 = 𝑇 ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧) = (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧))
1110ineq2d 3965 . . . . . . . 8 (𝑡 = 𝑇 → ((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)) = ((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)))
1211oteq1d 4551 . . . . . . 7 (𝑡 = 𝑇 → ⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩ = ⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
1312csbeq2dv 4136 . . . . . 6 (𝑡 = 𝑇(2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩ = (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
1413csbeq2dv 4136 . . . . 5 (𝑡 = 𝑇(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩ = (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
154, 14mpteq12dv 4867 . . . 4 (𝑡 = 𝑇 → (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
16 df-msr 31722 . . . 4 mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
173fvexi 6341 . . . . 5 𝑃 ∈ V
1817mptex 6628 . . . 4 (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩) ∈ V
1915, 16, 18fvmpt 6422 . . 3 (𝑇 ∈ V → (mStRed‘𝑇) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
20 mpt0 6159 . . . . 5 (𝑠 ∈ ∅ ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩) = ∅
2120eqcomi 2780 . . . 4 ∅ = (𝑠 ∈ ∅ ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
22 fvprc 6324 . . . 4 𝑇 ∈ V → (mStRed‘𝑇) = ∅)
23 fvprc 6324 . . . . . 6 𝑇 ∈ V → (mPreSt‘𝑇) = ∅)
243, 23syl5eq 2817 . . . . 5 𝑇 ∈ V → 𝑃 = ∅)
2524mpteq1d 4872 . . . 4 𝑇 ∈ V → (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩) = (𝑠 ∈ ∅ ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
2621, 22, 253eqtr4a 2831 . . 3 𝑇 ∈ V → (mStRed‘𝑇) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
2719, 26pm2.61i 176 . 2 (mStRed‘𝑇) = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
281, 27eqtri 2793 1 𝑅 = (𝑠𝑃(2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ (𝑉 “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1631  wcel 2145  Vcvv 3351  csb 3682  cun 3721  cin 3722  c0 4063  {csn 4316  cotp 4324   cuni 4574  cmpt 4863   × cxp 5247  cima 5252  cfv 6029  1st c1st 7311  2nd c2nd 7312  mVarscmvrs 31697  mPreStcmpst 31701  mStRedcmsr 31702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-ot 4325  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-msr 31722
This theorem is referenced by:  msrval  31766  msrf  31770
  Copyright terms: Public domain W3C validator