Metamath Proof Explorer

Theorem msrval

Description: Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msrfval.v 
|- V = ( mVars ` T )
msrfval.p 
|- P = ( mPreSt ` T )
msrfval.r 
|- R = ( mStRed ` T )
msrval.z 
|- Z = U. ( V " ( H u. { A } ) )
Assertion msrval 
|- ( <. D , H , A >. e. P -> ( R ` <. D , H , A >. ) = <. ( D i^i ( Z X. Z ) ) , H , A >. )

Proof

Step Hyp Ref Expression
1 msrfval.v 
 |-  V = ( mVars ` T )
2 msrfval.p 
 |-  P = ( mPreSt ` T )
3 msrfval.r 
 |-  R = ( mStRed ` T )
4 msrval.z 
 |-  Z = U. ( V " ( H u. { A } ) )
5 1 2 3 msrfval 
 |-  R = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
6 5 a1i 
 |-  ( <. D , H , A >. e. P -> R = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )
7 fvexd 
 |-  ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) -> ( 2nd ` ( 1st ` s ) ) e. _V )
8 fvexd 
 |-  ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) -> ( 2nd ` s ) e. _V )
9 simpllr 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> s = <. D , H , A >. )
10 9 fveq2d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 1st ` s ) = ( 1st ` <. D , H , A >. ) )
11 10 fveq2d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 1st ` ( 1st ` s ) ) = ( 1st ` ( 1st ` <. D , H , A >. ) ) )
12 eqid 
 |-  ( mDV ` T ) = ( mDV ` T )
13 eqid 
 |-  ( mEx ` T ) = ( mEx ` T )
14 12 13 2 elmpst 
 |-  ( <. D , H , A >. e. P <-> ( ( D C_ ( mDV ` T ) /\ `' D = D ) /\ ( H C_ ( mEx ` T ) /\ H e. Fin ) /\ A e. ( mEx ` T ) ) )
15 14 simp1bi 
 |-  ( <. D , H , A >. e. P -> ( D C_ ( mDV ` T ) /\ `' D = D ) )
16 15 simpld 
 |-  ( <. D , H , A >. e. P -> D C_ ( mDV ` T ) )
17 16 ad3antrrr 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> D C_ ( mDV ` T ) )
18 fvex 
 |-  ( mDV ` T ) e. _V
19 18 ssex 
 |-  ( D C_ ( mDV ` T ) -> D e. _V )
20 17 19 syl 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> D e. _V )
21 14 simp2bi 
 |-  ( <. D , H , A >. e. P -> ( H C_ ( mEx ` T ) /\ H e. Fin ) )
22 21 simprd 
 |-  ( <. D , H , A >. e. P -> H e. Fin )
23 22 ad3antrrr 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> H e. Fin )
24 14 simp3bi 
 |-  ( <. D , H , A >. e. P -> A e. ( mEx ` T ) )
25 24 ad3antrrr 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> A e. ( mEx ` T ) )
26 ot1stg 
 |-  ( ( D e. _V /\ H e. Fin /\ A e. ( mEx ` T ) ) -> ( 1st ` ( 1st ` <. D , H , A >. ) ) = D )
27 20 23 25 26 syl3anc 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 1st ` ( 1st ` <. D , H , A >. ) ) = D )
28 11 27 eqtrd 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 1st ` ( 1st ` s ) ) = D )
29 1 fvexi 
 |-  V e. _V
30 imaexg 
 |-  ( V e. _V -> ( V " ( h u. { a } ) ) e. _V )
31 29 30 ax-mp 
 |-  ( V " ( h u. { a } ) ) e. _V
32 31 uniex 
 |-  U. ( V " ( h u. { a } ) ) e. _V
33 32 a1i 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> U. ( V " ( h u. { a } ) ) e. _V )
34 id 
 |-  ( z = U. ( V " ( h u. { a } ) ) -> z = U. ( V " ( h u. { a } ) ) )
35 simplr 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> h = ( 2nd ` ( 1st ` s ) ) )
36 10 fveq2d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 2nd ` ( 1st ` s ) ) = ( 2nd ` ( 1st ` <. D , H , A >. ) ) )
37 ot2ndg 
 |-  ( ( D e. _V /\ H e. Fin /\ A e. ( mEx ` T ) ) -> ( 2nd ` ( 1st ` <. D , H , A >. ) ) = H )
38 20 23 25 37 syl3anc 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 2nd ` ( 1st ` <. D , H , A >. ) ) = H )
39 35 36 38 3eqtrd 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> h = H )
40 simpr 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> a = ( 2nd ` s ) )
41 9 fveq2d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 2nd ` s ) = ( 2nd ` <. D , H , A >. ) )
42 ot3rdg 
 |-  ( A e. ( mEx ` T ) -> ( 2nd ` <. D , H , A >. ) = A )
43 25 42 syl 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( 2nd ` <. D , H , A >. ) = A )
44 40 41 43 3eqtrd 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> a = A )
45 44 sneqd 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> { a } = { A } )
46 39 45 uneq12d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( h u. { a } ) = ( H u. { A } ) )
47 46 imaeq2d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( V " ( h u. { a } ) ) = ( V " ( H u. { A } ) ) )
48 47 unieqd 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> U. ( V " ( h u. { a } ) ) = U. ( V " ( H u. { A } ) ) )
49 48 4 eqtr4di 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> U. ( V " ( h u. { a } ) ) = Z )
50 34 49 sylan9eqr 
 |-  ( ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) /\ z = U. ( V " ( h u. { a } ) ) ) -> z = Z )
51 50 sqxpeqd 
 |-  ( ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) /\ z = U. ( V " ( h u. { a } ) ) ) -> ( z X. z ) = ( Z X. Z ) )
52 33 51 csbied 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) = ( Z X. Z ) )
53 28 52 ineq12d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) = ( D i^i ( Z X. Z ) ) )
54 53 39 44 oteq123d 
 |-  ( ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) /\ a = ( 2nd ` s ) ) -> <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. = <. ( D i^i ( Z X. Z ) ) , H , A >. )
55 8 54 csbied 
 |-  ( ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) /\ h = ( 2nd ` ( 1st ` s ) ) ) -> [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. = <. ( D i^i ( Z X. Z ) ) , H , A >. )
56 7 55 csbied 
 |-  ( ( <. D , H , A >. e. P /\ s = <. D , H , A >. ) -> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. = <. ( D i^i ( Z X. Z ) ) , H , A >. )
57 id 
 |-  ( <. D , H , A >. e. P -> <. D , H , A >. e. P )
58 otex 
 |-  <. ( D i^i ( Z X. Z ) ) , H , A >. e. _V
59 58 a1i 
 |-  ( <. D , H , A >. e. P -> <. ( D i^i ( Z X. Z ) ) , H , A >. e. _V )
60 6 56 57 59 fvmptd 
 |-  ( <. D , H , A >. e. P -> ( R ` <. D , H , A >. ) = <. ( D i^i ( Z X. Z ) ) , H , A >. )