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 31132
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 6150 . . . . . . . . 9 (𝑡 = 𝑇 → (mDV‘𝑡) = (mDV‘𝑇))
3 mpstval.v . . . . . . . . 9 𝑉 = (mDV‘𝑇)
42, 3syl6eqr 2678 . . . . . . . 8 (𝑡 = 𝑇 → (mDV‘𝑡) = 𝑉)
54pweqd 4140 . . . . . . 7 (𝑡 = 𝑇 → 𝒫 (mDV‘𝑡) = 𝒫 𝑉)
65rabeqdv 3185 . . . . . 6 (𝑡 = 𝑇 → {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} = {𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑})
7 fveq2 6150 . . . . . . . . 9 (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇))
8 mpstval.e . . . . . . . . 9 𝐸 = (mEx‘𝑇)
97, 8syl6eqr 2678 . . . . . . . 8 (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸)
109pweqd 4140 . . . . . . 7 (𝑡 = 𝑇 → 𝒫 (mEx‘𝑡) = 𝒫 𝐸)
1110ineq1d 3796 . . . . . 6 (𝑡 = 𝑇 → (𝒫 (mEx‘𝑡) ∩ Fin) = (𝒫 𝐸 ∩ Fin))
126, 11xpeq12d 5105 . . . . 5 (𝑡 = 𝑇 → ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) = ({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)))
1312, 9xpeq12d 5105 . . . 4 (𝑡 = 𝑇 → (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸))
14 df-mpst 31090 . . . 4 mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
15 fvex 6160 . . . . . . . . 9 (mDV‘𝑇) ∈ V
163, 15eqeltri 2700 . . . . . . . 8 𝑉 ∈ V
1716pwex 4813 . . . . . . 7 𝒫 𝑉 ∈ V
1817rabex 4778 . . . . . 6 {𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} ∈ V
19 fvex 6160 . . . . . . . . 9 (mEx‘𝑇) ∈ V
208, 19eqeltri 2700 . . . . . . . 8 𝐸 ∈ V
2120pwex 4813 . . . . . . 7 𝒫 𝐸 ∈ V
2221inex1 4764 . . . . . 6 (𝒫 𝐸 ∩ Fin) ∈ V
2318, 22xpex 6916 . . . . 5 ({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ∈ V
2423, 20xpex 6916 . . . 4 (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) ∈ V
2513, 14, 24fvmpt 6240 . . 3 (𝑇 ∈ V → (mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸))
26 xp0 5515 . . . . 5 (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × ∅) = ∅
2726eqcomi 2635 . . . 4 ∅ = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × ∅)
28 fvprc 6144 . . . 4 𝑇 ∈ V → (mPreSt‘𝑇) = ∅)
29 fvprc 6144 . . . . . 6 𝑇 ∈ V → (mEx‘𝑇) = ∅)
308, 29syl5eq 2672 . . . . 5 𝑇 ∈ V → 𝐸 = ∅)
3130xpeq2d 5104 . . . 4 𝑇 ∈ V → (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × ∅))
3227, 28, 313eqtr4a 2686 . . 3 𝑇 ∈ V → (mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸))
3325, 32pm2.61i 176 . 2 (mPreSt‘𝑇) = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)
341, 33eqtri 2648 1 𝑃 = (({𝑑 ∈ 𝒫 𝑉𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1480  wcel 1992  {crab 2916  Vcvv 3191  cin 3559  c0 3896  𝒫 cpw 4135   × cxp 5077  ccnv 5078  cfv 5850  Fincfn 7900  mExcmex 31064  mDVcmdv 31065  mPreStcmpst 31070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-iota 5813  df-fun 5852  df-fv 5858  df-mpst 31090
This theorem is referenced by:  elmpst  31133  mpstssv  31136
  Copyright terms: Public domain W3C validator