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

Theorem mpstval 31764
Description: A pre-statement is an ordered triple, whose first member is a symmetric set of dv conditions, whose second member is a finite set of expressions, and whose third member is an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mpstval.v 𝑉 = (mDV‘𝑇)
mpstval.e 𝐸 = (mEx‘𝑇)
mpstval.p 𝑃 = (mPreSt‘𝑇)
Assertion
Ref Expression
mpstval 𝑃 = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)
Distinct variable groups:   𝑇,𝑑   𝑉,𝑑
Allowed substitution hints:   𝑃(𝑑)   𝐸(𝑑)

Proof of Theorem mpstval
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 mpstval.p . 2 𝑃 = (mPreSt‘𝑇)
2 fveq2 6332 . . . . . . . . 9 (𝑡 = 𝑇 → (mDV‘𝑡) = (mDV‘𝑇))
3 mpstval.v . . . . . . . . 9 𝑉 = (mDV‘𝑇)
42, 3syl6eqr 2822 . . . . . . . 8 (𝑡 = 𝑇 → (mDV‘𝑡) = 𝑉)
54pweqd 4300 . . . . . . 7 (𝑡 = 𝑇 → 𝒫 (mDV‘𝑡) = 𝒫 𝑉)
65rabeqdv 3343 . . . . . 6 (𝑡 = 𝑇 → {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} = {𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑})
7 fveq2 6332 . . . . . . . . 9 (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇))
8 mpstval.e . . . . . . . . 9 𝐸 = (mEx‘𝑇)
97, 8syl6eqr 2822 . . . . . . . 8 (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸)
109pweqd 4300 . . . . . . 7 (𝑡 = 𝑇 → 𝒫 (mEx‘𝑡) = 𝒫 𝐸)
1110ineq1d 3962 . . . . . 6 (𝑡 = 𝑇 → (𝒫 (mEx‘𝑡) ∩ Fin) = (𝒫 𝐸 ∩ Fin))
126, 11xpeq12d 5280 . . . . 5 (𝑡 = 𝑇 → ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) = ({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)))
1312, 9xpeq12d 5280 . . . 4 (𝑡 = 𝑇 → (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸))
14 df-mpst 31722 . . . 4 mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
15 fvex 6342 . . . . . . . . 9 (mDV‘𝑇) ∈ V
163, 15eqeltri 2845 . . . . . . . 8 𝑉 ∈ V
1716pwex 4976 . . . . . . 7 𝒫 𝑉 ∈ V
1817rabex 4943 . . . . . 6 {𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} ∈ V
19 fvex 6342 . . . . . . . . 9 (mEx‘𝑇) ∈ V
208, 19eqeltri 2845 . . . . . . . 8 𝐸 ∈ V
2120pwex 4976 . . . . . . 7 𝒫 𝐸 ∈ V
2221inex1 4930 . . . . . 6 (𝒫 𝐸 ∩ Fin) ∈ V
2318, 22xpex 7108 . . . . 5 ({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ∈ V
2423, 20xpex 7108 . . . 4 (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) ∈ V
2513, 14, 24fvmpt 6424 . . 3 (𝑇 ∈ V → (mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸))
26 xp0 5693 . . . . 5 (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × ∅) = ∅
2726eqcomi 2779 . . . 4 ∅ = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × ∅)
28 fvprc 6326 . . . 4 𝑇 ∈ V → (mPreSt‘𝑇) = ∅)
29 fvprc 6326 . . . . . 6 𝑇 ∈ V → (mEx‘𝑇) = ∅)
308, 29syl5eq 2816 . . . . 5 𝑇 ∈ V → 𝐸 = ∅)
3130xpeq2d 5279 . . . 4 𝑇 ∈ V → (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × ∅))
3227, 28, 313eqtr4a 2830 . . 3 𝑇 ∈ V → (mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸))
3325, 32pm2.61i 176 . 2 (mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)
341, 33eqtri 2792 1 𝑃 = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1630  wcel 2144  {crab 3064  Vcvv 3349  cin 3720  c0 4061  𝒫 cpw 4295   × cxp 5247  ccnv 5248  cfv 6031  Fincfn 8108  mExcmex 31696  mDVcmdv 31697  mPreStcmpst 31702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-mpst 31722
This theorem is referenced by:  elmpst  31765  mpstssv  31768
  Copyright terms: Public domain W3C validator