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

Theorem mpstval 29961
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  |-  V  =  (mDV `  T )
mpstval.e  |-  E  =  (mEx `  T )
mpstval.p  |-  P  =  (mPreSt `  T )
Assertion
Ref Expression
mpstval  |-  P  =  ( ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E )
Distinct variable groups:    T, d    V, d
Allowed substitution hints:    P( d)    E( d)

Proof of Theorem mpstval
Dummy variable  t is distinct from all other variables.
StepHypRef Expression
1 mpstval.p . 2  |-  P  =  (mPreSt `  T )
2 fveq2 5881 . . . . . . . . 9  |-  ( t  =  T  ->  (mDV `  t )  =  (mDV
`  T ) )
3 mpstval.v . . . . . . . . 9  |-  V  =  (mDV `  T )
42, 3syl6eqr 2488 . . . . . . . 8  |-  ( t  =  T  ->  (mDV `  t )  =  V )
54pweqd 3990 . . . . . . 7  |-  ( t  =  T  ->  ~P (mDV `  t )  =  ~P V )
6 biidd 240 . . . . . . 7  |-  ( t  =  T  ->  ( `' d  =  d  <->  `' d  =  d ) )
75, 6rabeqbidv 3082 . . . . . 6  |-  ( t  =  T  ->  { d  e.  ~P (mDV `  t )  |  `' d  =  d }  =  { d  e.  ~P V  |  `' d  =  d } )
8 fveq2 5881 . . . . . . . . 9  |-  ( t  =  T  ->  (mEx `  t )  =  (mEx
`  T ) )
9 mpstval.e . . . . . . . . 9  |-  E  =  (mEx `  T )
108, 9syl6eqr 2488 . . . . . . . 8  |-  ( t  =  T  ->  (mEx `  t )  =  E )
1110pweqd 3990 . . . . . . 7  |-  ( t  =  T  ->  ~P (mEx `  t )  =  ~P E )
1211ineq1d 3669 . . . . . 6  |-  ( t  =  T  ->  ( ~P (mEx `  t )  i^i  Fin )  =  ( ~P E  i^i  Fin ) )
137, 12xpeq12d 4879 . . . . 5  |-  ( t  =  T  ->  ( { d  e.  ~P (mDV `  t )  |  `' d  =  d }  X.  ( ~P (mEx `  t )  i^i  Fin ) )  =  ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) ) )
1413, 10xpeq12d 4879 . . . 4  |-  ( t  =  T  ->  (
( { d  e. 
~P (mDV `  t
)  |  `' d  =  d }  X.  ( ~P (mEx `  t
)  i^i  Fin )
)  X.  (mEx `  t ) )  =  ( ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E ) )
15 df-mpst 29919 . . . 4  |- mPreSt  =  ( t  e.  _V  |->  ( ( { d  e. 
~P (mDV `  t
)  |  `' d  =  d }  X.  ( ~P (mEx `  t
)  i^i  Fin )
)  X.  (mEx `  t ) ) )
16 fvex 5891 . . . . . . . . 9  |-  (mDV `  T )  e.  _V
173, 16eqeltri 2513 . . . . . . . 8  |-  V  e. 
_V
1817pwex 4608 . . . . . . 7  |-  ~P V  e.  _V
1918rabex 4576 . . . . . 6  |-  { d  e.  ~P V  |  `' d  =  d }  e.  _V
20 fvex 5891 . . . . . . . . 9  |-  (mEx `  T )  e.  _V
219, 20eqeltri 2513 . . . . . . . 8  |-  E  e. 
_V
2221pwex 4608 . . . . . . 7  |-  ~P E  e.  _V
2322inex1 4566 . . . . . 6  |-  ( ~P E  i^i  Fin )  e.  _V
2419, 23xpex 6609 . . . . 5  |-  ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  e. 
_V
2524, 21xpex 6609 . . . 4  |-  ( ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E
)  e.  _V
2614, 15, 25fvmpt 5964 . . 3  |-  ( T  e.  _V  ->  (mPreSt `  T )  =  ( ( { d  e. 
~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E
) )
27 xp0 5275 . . . . 5  |-  ( ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  (/) )  =  (/)
2827eqcomi 2442 . . . 4  |-  (/)  =  ( ( { d  e. 
~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  (/) )
29 fvprc 5875 . . . 4  |-  ( -.  T  e.  _V  ->  (mPreSt `  T )  =  (/) )
30 fvprc 5875 . . . . . 6  |-  ( -.  T  e.  _V  ->  (mEx
`  T )  =  (/) )
319, 30syl5eq 2482 . . . . 5  |-  ( -.  T  e.  _V  ->  E  =  (/) )
3231xpeq2d 4878 . . . 4  |-  ( -.  T  e.  _V  ->  ( ( { d  e. 
~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E
)  =  ( ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  (/) ) )
3328, 29, 323eqtr4a 2496 . . 3  |-  ( -.  T  e.  _V  ->  (mPreSt `  T )  =  ( ( { d  e. 
~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E
) )
3426, 33pm2.61i 167 . 2  |-  (mPreSt `  T )  =  ( ( { d  e. 
~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E
)
351, 34eqtri 2458 1  |-  P  =  ( ( { d  e.  ~P V  |  `' d  =  d }  X.  ( ~P E  i^i  Fin ) )  X.  E )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1437    e. wcel 1870   {crab 2786   _Vcvv 3087    i^i cin 3441   (/)c0 3767   ~Pcpw 3985    X. cxp 4852   `'ccnv 4853   ` cfv 5601   Fincfn 7577  mExcmex 29893  mDVcmdv 29894  mPreStcmpst 29899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-iota 5565  df-fun 5603  df-fv 5609  df-mpst 29919
This theorem is referenced by:  elmpst  29962  mpstssv  29965
  Copyright terms: Public domain W3C validator