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	⊢ 𝑉 = ( mDV ‘ 𝑇 )
	mpstval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mpstval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
Assertion	mpstval	⊢ 𝑃 = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		mpstval.v	⊢ 𝑉 = ( mDV ‘ 𝑇 )
2		mpstval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mpstval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
4		fveq2	⊢ ( 𝑡 = 𝑇 → ( mDV ‘ 𝑡 ) = ( mDV ‘ 𝑇 ) )
5	4 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mDV ‘ 𝑡 ) = 𝑉 )
6	5	pweqd	⊢ ( 𝑡 = 𝑇 → 𝒫 ( mDV ‘ 𝑡 ) = 𝒫 𝑉 )
7	6	rabeqdv	⊢ ( 𝑡 = 𝑇 → { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } = { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } )
8		fveq2	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = ( mEx ‘ 𝑇 ) )
9	8 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = 𝐸 )
10	9	pweqd	⊢ ( 𝑡 = 𝑇 → 𝒫 ( mEx ‘ 𝑡 ) = 𝒫 𝐸 )
11	10	ineq1d	⊢ ( 𝑡 = 𝑇 → ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) = ( 𝒫 𝐸 ∩ Fin ) )
12	7 11	xpeq12d	⊢ ( 𝑡 = 𝑇 → ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) ) = ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) )
13	12 9	xpeq12d	⊢ ( 𝑡 = 𝑇 → ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) ) × ( mEx ‘ 𝑡 ) ) = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) )
14		df-mpst	⊢ mPreSt = ( 𝑡 ∈ V ↦ ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) ) × ( mEx ‘ 𝑡 ) ) )
15	1	fvexi	⊢ 𝑉 ∈ V
16	15	pwex	⊢ 𝒫 𝑉 ∈ V
17	16	rabex	⊢ { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } ∈ V
18	2	fvexi	⊢ 𝐸 ∈ V
19	18	pwex	⊢ 𝒫 𝐸 ∈ V
20	19	inex1	⊢ ( 𝒫 𝐸 ∩ Fin ) ∈ V
21	17 20	xpex	⊢ ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) ∈ V
22	21 18	xpex	⊢ ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) ∈ V
23	13 14 22	fvmpt	⊢ ( 𝑇 ∈ V → ( mPreSt ‘ 𝑇 ) = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) )
24		xp0	⊢ ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × ∅ ) = ∅
25	24	eqcomi	⊢ ∅ = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × ∅ )
26		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mPreSt ‘ 𝑇 ) = ∅ )
27		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mEx ‘ 𝑇 ) = ∅ )
28	2 27	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝐸 = ∅ )
29	28	xpeq2d	⊢ ( ¬ 𝑇 ∈ V → ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × ∅ ) )
30	25 26 29	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( mPreSt ‘ 𝑇 ) = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) )
31	23 30	pm2.61i	⊢ ( mPreSt ‘ 𝑇 ) = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 )
32	3 31	eqtri	⊢ 𝑃 = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 )