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=\mathrm{mDV}\left(T\right)$$
	mpstval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
	mpstval.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
Assertion	mpstval	$$⊢P=\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E$$

Proof

Step	Hyp	Ref	Expression
1		mpstval.v	$$⊢V=\mathrm{mDV}\left(T\right)$$
2		mpstval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
3		mpstval.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
4		fveq2	$$⊢t=T\to \mathrm{mDV}\left(t\right)=\mathrm{mDV}\left(T\right)$$
5	4 1	eqtr4di	$$⊢t=T\to \mathrm{mDV}\left(t\right)=V$$
6	5	pweqd	$$⊢t=T\to 𝒫\mathrm{mDV}\left(t\right)=𝒫V$$
7	6	rabeqdv	$$⊢t=T\to \left\{d\in 𝒫\mathrm{mDV}\left(t\right)|d^{-1}=d\right\}=\left\{d\in 𝒫V|d^{-1}=d\right\}$$
8		fveq2	$$⊢t=T\to \mathrm{mEx}\left(t\right)=\mathrm{mEx}\left(T\right)$$
9	8 2	eqtr4di	$$⊢t=T\to \mathrm{mEx}\left(t\right)=E$$
10	9	pweqd	$$⊢t=T\to 𝒫\mathrm{mEx}\left(t\right)=𝒫E$$
11	10	ineq1d	$$⊢t=T\to 𝒫\mathrm{mEx}\left(t\right)\cap \mathrm{Fin}=𝒫E\cap \mathrm{Fin}$$
12	7 11	xpeq12d	$$⊢t=T\to \left\{d\in 𝒫\mathrm{mDV}\left(t\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(t\right)\cap \mathrm{Fin}\right)=\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)$$
13	12 9	xpeq12d	$$⊢t=T\to \left(\left\{d\in 𝒫\mathrm{mDV}\left(t\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(t\right)\cap \mathrm{Fin}\right)\right)\times \mathrm{mEx}\left(t\right)=\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E$$
14		df-mpst	$$⊢\mathrm{mPreSt}=\left(t\in \mathrm{V}⟼\left(\left\{d\in 𝒫\mathrm{mDV}\left(t\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(t\right)\cap \mathrm{Fin}\right)\right)\times \mathrm{mEx}\left(t\right)\right)$$
15	1	fvexi	$$⊢V\in \mathrm{V}$$
16	15	pwex	$$⊢𝒫V\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{d\in 𝒫V|d^{-1}=d\right\}\in \mathrm{V}$$
18	2	fvexi	$$⊢E\in \mathrm{V}$$
19	18	pwex	$$⊢𝒫E\in \mathrm{V}$$
20	19	inex1	$$⊢𝒫E\cap \mathrm{Fin}\in \mathrm{V}$$
21	17 20	xpex	$$⊢\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\in \mathrm{V}$$
22	21 18	xpex	$$⊢\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E\in \mathrm{V}$$
23	13 14 22	fvmpt	$$⊢T\in \mathrm{V}\to \mathrm{mPreSt}\left(T\right)=\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E$$
24		xp0	$$⊢\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times \varnothing =\varnothing$$
25	24	eqcomi	$$⊢\varnothing =\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times \varnothing$$
26		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mPreSt}\left(T\right)=\varnothing$$
27		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mEx}\left(T\right)=\varnothing$$
28	2 27	eqtrid	$$⊢\neg T\in \mathrm{V}\to E=\varnothing$$
29	28	xpeq2d	$$⊢\neg T\in \mathrm{V}\to \left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E=\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times \varnothing$$
30	25 26 29	3eqtr4a	$$⊢\neg T\in \mathrm{V}\to \mathrm{mPreSt}\left(T\right)=\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E$$
31	23 30	pm2.61i	$$⊢\mathrm{mPreSt}\left(T\right)=\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E$$
32	3 31	eqtri	$$⊢P=\left(\left\{d\in 𝒫V|d^{-1}=d\right\}\times \left(𝒫E\cap \mathrm{Fin}\right)\right)\times E$$