# 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}=\mathrm{mVars}\left({T}\right)$
msrfval.p ${⊢}{P}=\mathrm{mPreSt}\left({T}\right)$
msrfval.r ${⊢}{R}=\mathrm{mStRed}\left({T}\right)$
msrval.z ${⊢}{Z}=\bigcup {V}\left[{H}\cup \left\{{A}\right\}\right]$
Assertion msrval ${⊢}⟨{D},{H},{A}⟩\in {P}\to {R}\left(⟨{D},{H},{A}⟩\right)=⟨{D}\cap \left({Z}×{Z}\right),{H},{A}⟩$

### Proof

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