Metamath Proof Explorer

Theorem mpstval

Description: A pre-statement is an ordered triple, whose first member is a symmetric set of disjoint variable conditions, whose second member is a finite set of expressions, and whose third member is an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mpstval.v 
|- V = ( mDV ` T )
mpstval.e 
|- E = ( mEx ` T )
mpstval.p 
|- P = ( mPreSt ` T )
Assertion mpstval 
|- P = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E )

Proof

Step Hyp Ref Expression
1 mpstval.v 
 |-  V = ( mDV ` T )
2 mpstval.e 
 |-  E = ( mEx ` T )
3 mpstval.p 
 |-  P = ( mPreSt ` T )
4 fveq2 
 |-  ( t = T -> ( mDV ` t ) = ( mDV ` T ) )
5 4 1 eqtr4di 
 |-  ( t = T -> ( mDV ` t ) = V )
6 5 pweqd 
 |-  ( t = T -> ~P ( mDV ` t ) = ~P V )
7 6 rabeqdv 
 |-  ( t = T -> { d e. ~P ( mDV ` t ) | `' d = d } = { d e. ~P V | `' d = d } )
8 fveq2 
 |-  ( t = T -> ( mEx ` t ) = ( mEx ` T ) )
9 8 2 eqtr4di 
 |-  ( t = T -> ( mEx ` t ) = E )
10 9 pweqd 
 |-  ( t = T -> ~P ( mEx ` t ) = ~P E )
11 10 ineq1d 
 |-  ( t = T -> ( ~P ( mEx ` t ) i^i Fin ) = ( ~P E i^i Fin ) )
12 7 11 xpeq12d 
 |-  ( 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 ) ) )
13 12 9 xpeq12d 
 |-  ( 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 ) )
14 df-mpst 
 |-  mPreSt = ( t e. _V |-> ( ( { d e. ~P ( mDV ` t ) | `' d = d } X. ( ~P ( mEx ` t ) i^i Fin ) ) X. ( mEx ` t ) ) )
15 1 fvexi 
 |-  V e. _V
16 15 pwex 
 |-  ~P V e. _V
17 16 rabex 
 |-  { d e. ~P V | `' d = d } e. _V
18 2 fvexi 
 |-  E e. _V
19 18 pwex 
 |-  ~P E e. _V
20 19 inex1 
 |-  ( ~P E i^i Fin ) e. _V
21 17 20 xpex 
 |-  ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) e. _V
22 21 18 xpex 
 |-  ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E ) e. _V
23 13 14 22 fvmpt 
 |-  ( T e. _V -> ( mPreSt ` T ) = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E ) )
24 xp0 
 |-  ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. (/) ) = (/)
25 24 eqcomi 
 |-  (/) = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. (/) )
26 fvprc 
 |-  ( -. T e. _V -> ( mPreSt ` T ) = (/) )
27 fvprc 
 |-  ( -. T e. _V -> ( mEx ` T ) = (/) )
28 2 27 syl5eq 
 |-  ( -. T e. _V -> E = (/) )
29 28 xpeq2d 
 |-  ( -. 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. (/) ) )
30 25 26 29 3eqtr4a 
 |-  ( -. T e. _V -> ( mPreSt ` T ) = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E ) )
31 23 30 pm2.61i 
 |-  ( mPreSt ` T ) = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E )
32 3 31 eqtri 
 |-  P = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E )