Metamath Proof Explorer

Theorem elmpst

Description: Property of being a pre-statement. (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 elmpst 
|- ( <. D , H , A >. e. P <-> ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) /\ A e. 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 opelxp 
 |-  ( <. <. D , H >. , A >. e. ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E ) <-> ( <. D , H >. e. ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) /\ A e. E ) )
5 opelxp 
 |-  ( <. D , H >. e. ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) <-> ( D e. { d e. ~P V | `' d = d } /\ H e. ( ~P E i^i Fin ) ) )
6 cnveq 
 |-  ( d = D -> `' d = `' D )
7 id 
 |-  ( d = D -> d = D )
8 6 7 eqeq12d 
 |-  ( d = D -> ( `' d = d <-> `' D = D ) )
9 8 elrab 
 |-  ( D e. { d e. ~P V | `' d = d } <-> ( D e. ~P V /\ `' D = D ) )
10 1 fvexi 
 |-  V e. _V
11 10 elpw2 
 |-  ( D e. ~P V <-> D C_ V )
12 11 anbi1i 
 |-  ( ( D e. ~P V /\ `' D = D ) <-> ( D C_ V /\ `' D = D ) )
13 9 12 bitri 
 |-  ( D e. { d e. ~P V | `' d = d } <-> ( D C_ V /\ `' D = D ) )
14 elfpw 
 |-  ( H e. ( ~P E i^i Fin ) <-> ( H C_ E /\ H e. Fin ) )
15 13 14 anbi12i 
 |-  ( ( D e. { d e. ~P V | `' d = d } /\ H e. ( ~P E i^i Fin ) ) <-> ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) ) )
16 5 15 bitri 
 |-  ( <. D , H >. e. ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) <-> ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) ) )
17 16 anbi1i 
 |-  ( ( <. D , H >. e. ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) /\ A e. E ) <-> ( ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) ) /\ A e. E ) )
18 4 17 bitri 
 |-  ( <. <. D , H >. , A >. e. ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E ) <-> ( ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) ) /\ A e. E ) )
19 df-ot 
 |-  <. D , H , A >. = <. <. D , H >. , A >.
20 1 2 3 mpstval 
 |-  P = ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E )
21 19 20 eleq12i 
 |-  ( <. D , H , A >. e. P <-> <. <. D , H >. , A >. e. ( ( { d e. ~P V | `' d = d } X. ( ~P E i^i Fin ) ) X. E ) )
22 df-3an 
 |-  ( ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) /\ A e. E ) <-> ( ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) ) /\ A e. E ) )
23 18 21 22 3bitr4i 
 |-  ( <. D , H , A >. e. P <-> ( ( D C_ V /\ `' D = D ) /\ ( H C_ E /\ H e. Fin ) /\ A e. E ) )