Definition df-msr 35499

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

Assertion

Ref	Expression
df-msr	⊢ mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩))

Distinct variable group:   ℎ,𝑎,𝑠,𝑡,𝑧

Detailed syntax breakdown of Definition df-msr

Step	Hyp	Ref	Expression
1		cmsr 35479	. 2 class mStRed
2		vt	. . 3 setvar 𝑡
3		cvv 3480	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1539	. . . . 5 class 𝑡
6		cmpst 35478	. . . . 5 class mPreSt
7	5, 6	cfv 6561	. . . 4 class (mPreSt‘𝑡)
8		vh	. . . . 5 setvar ℎ
9	4	cv 1539	. . . . . . 7 class 𝑠
10		c1st 8012	. . . . . . 7 class 1st
11	9, 10	cfv 6561	. . . . . 6 class (1st ‘𝑠)
12		c2nd 8013	. . . . . 6 class 2nd
13	11, 12	cfv 6561	. . . . 5 class (2nd ‘(1st ‘𝑠))
14		va	. . . . . 6 setvar 𝑎
15	9, 12	cfv 6561	. . . . . 6 class (2nd ‘𝑠)
16	11, 10	cfv 6561	. . . . . . . 8 class (1st ‘(1st ‘𝑠))
17		vz	. . . . . . . . 9 setvar 𝑧
18		cmvrs 35474	. . . . . . . . . . . 12 class mVars
19	5, 18	cfv 6561	. . . . . . . . . . 11 class (mVars‘𝑡)
20	8	cv 1539	. . . . . . . . . . . 12 class ℎ
21	14	cv 1539	. . . . . . . . . . . . 13 class 𝑎
22	21	csn 4626	. . . . . . . . . . . 12 class {𝑎}
23	20, 22	cun 3949	. . . . . . . . . . 11 class (ℎ ∪ {𝑎})
24	19, 23	cima 5688	. . . . . . . . . 10 class ((mVars‘𝑡) “ (ℎ ∪ {𝑎}))
25	24	cuni 4907	. . . . . . . . 9 class ∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎}))
26	17	cv 1539	. . . . . . . . . 10 class 𝑧
27	26, 26	cxp 5683	. . . . . . . . 9 class (𝑧 × 𝑧)
28	17, 25, 27	csb 3899	. . . . . . . 8 class ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)
29	16, 28	cin 3950	. . . . . . 7 class ((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧))
30	29, 20, 21	cotp 4634	. . . . . 6 class ⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩
31	14, 15, 30	csb 3899	. . . . 5 class ⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩
32	8, 13, 31	csb 3899	. . . 4 class ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩
33	4, 7, 32	cmpt 5225	. . 3 class (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩)
34	2, 3, 33	cmpt 5225	. 2 class (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩))
35	1, 34	wceq 1540	1 wff mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩))

This definition is referenced by:  msrfval  35542