Metamath Proof Explorer


Theorem elmsta

Description: Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mstapst.p P=mPreStT
mstapst.s S=mStatT
elmsta.v V=mVarsT
elmsta.z Z=VHA
Assertion elmsta DHASDHAPDZ×Z

Proof

Step Hyp Ref Expression
1 mstapst.p P=mPreStT
2 mstapst.s S=mStatT
3 elmsta.v V=mVarsT
4 elmsta.z Z=VHA
5 1 2 mstapst SP
6 5 sseli DHASDHAP
7 eqid mStRedT=mStRedT
8 3 1 7 4 msrval DHAPmStRedTDHA=DZ×ZHA
9 6 8 syl DHASmStRedTDHA=DZ×ZHA
10 7 2 msrid DHASmStRedTDHA=DHA
11 9 10 eqtr3d DHASDZ×ZHA=DHA
12 11 fveq2d DHAS1stDZ×ZHA=1stDHA
13 12 fveq2d DHAS1st1stDZ×ZHA=1st1stDHA
14 inss1 DZ×ZD
15 1 mpstrcl DHAPDVHVAV
16 6 15 syl DHASDVHVAV
17 16 simp1d DHASDV
18 ssexg DZ×ZDDVDZ×ZV
19 14 17 18 sylancr DHASDZ×ZV
20 16 simp2d DHASHV
21 16 simp3d DHASAV
22 ot1stg DZ×ZVHVAV1st1stDZ×ZHA=DZ×Z
23 19 20 21 22 syl3anc DHAS1st1stDZ×ZHA=DZ×Z
24 ot1stg DVHVAV1st1stDHA=D
25 16 24 syl DHAS1st1stDHA=D
26 13 23 25 3eqtr3d DHASDZ×Z=D
27 inss2 DZ×ZZ×Z
28 26 27 eqsstrrdi DHASDZ×Z
29 6 28 jca DHASDHAPDZ×Z
30 8 adantr DHAPDZ×ZmStRedTDHA=DZ×ZHA
31 simpr DHAPDZ×ZDZ×Z
32 df-ss DZ×ZDZ×Z=D
33 31 32 sylib DHAPDZ×ZDZ×Z=D
34 33 oteq1d DHAPDZ×ZDZ×ZHA=DHA
35 30 34 eqtrd DHAPDZ×ZmStRedTDHA=DHA
36 1 7 msrf mStRedT:PP
37 ffn mStRedT:PPmStRedTFnP
38 36 37 ax-mp mStRedTFnP
39 simpl DHAPDZ×ZDHAP
40 fnfvelrn mStRedTFnPDHAPmStRedTDHAranmStRedT
41 38 39 40 sylancr DHAPDZ×ZmStRedTDHAranmStRedT
42 35 41 eqeltrrd DHAPDZ×ZDHAranmStRedT
43 7 2 mstaval S=ranmStRedT
44 42 43 eleqtrrdi DHAPDZ×ZDHAS
45 29 44 impbii DHASDHAPDZ×Z