df-msr - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-msr		Structured version Visualization version GIF version

Definition df-msr 34516

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

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

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

**Detailed syntax breakdown of Definition df-msr**
Step	Hyp	Ref	Expression
1		cmsr 34496	. 2 class mStRed
2		vt	. . 3 setvar 𝑡
3		cvv 3475	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1541	. . . . 5 class 𝑡
6		cmpst 34495	. . . . 5 class mPreSt
7	5, 6	cfv 6544	. . . 4 class (mPreSt‘𝑡)
8		vh	. . . . 5 setvar ℎ
9	4	cv 1541	. . . . . . 7 class 𝑠
10		c1st 7973	. . . . . . 7 class 1^st
11	9, 10	cfv 6544	. . . . . 6 class (1^st ‘𝑠)
12		c2nd 7974	. . . . . 6 class 2^nd
13	11, 12	cfv 6544	. . . . 5 class (2^nd ‘(1^st ‘𝑠))
14		va	. . . . . 6 setvar 𝑎
15	9, 12	cfv 6544	. . . . . 6 class (2^nd ‘𝑠)
16	11, 10	cfv 6544	. . . . . . . 8 class (1^st ‘(1^st ‘𝑠))
17		vz	. . . . . . . . 9 setvar 𝑧
18		cmvrs 34491	. . . . . . . . . . . 12 class mVars
19	5, 18	cfv 6544	. . . . . . . . . . 11 class (mVars‘𝑡)
20	8	cv 1541	. . . . . . . . . . . 12 class ℎ
21	14	cv 1541	. . . . . . . . . . . . 13 class 𝑎
22	21	csn 4629	. . . . . . . . . . . 12 class {𝑎}
23	20, 22	cun 3947	. . . . . . . . . . 11 class (ℎ ∪ {𝑎})
24	19, 23	cima 5680	. . . . . . . . . 10 class ((mVars‘𝑡) “ (ℎ ∪ {𝑎}))
25	24	cuni 4909	. . . . . . . . 9 class ∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎}))
26	17	cv 1541	. . . . . . . . . 10 class 𝑧
27	26, 26	cxp 5675	. . . . . . . . 9 class (𝑧 × 𝑧)
28	17, 25, 27	csb 3894	. . . . . . . 8 class ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)
29	16, 28	cin 3948	. . . . . . 7 class ((1^st ‘(1^st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧))
30	29, 20, 21	cotp 4637	. . . . . 6 class ⟨((1^st ‘(1^st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩
31	14, 15, 30	csb 3894	. . . . 5 class ⦋(2^nd ‘𝑠) / 𝑎⦌⟨((1^st ‘(1^st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩
32	8, 13, 31	csb 3894	. . . 4 class ⦋(2^nd ‘(1^st ‘𝑠)) / ℎ⦌⦋(2^nd ‘𝑠) / 𝑎⦌⟨((1^st ‘(1^st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩
33	4, 7, 32	cmpt 5232	. . 3 class (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2^nd ‘(1^st ‘𝑠)) / ℎ⦌⦋(2^nd ‘𝑠) / 𝑎⦌⟨((1^st ‘(1^st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩)
34	2, 3, 33	cmpt 5232	. 2 class (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2^nd ‘(1^st ‘𝑠)) / ℎ⦌⦋(2^nd ‘𝑠) / 𝑎⦌⟨((1^st ‘(1^st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩))
35	1, 34	wceq 1542	1 wff mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2^nd ‘(1^st ‘𝑠)) / ℎ⦌⦋(2^nd ‘𝑠) / 𝑎⦌⟨((1^st ‘(1^st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩))

Colors of variables: wff setvar class

This definition is referenced by: msrfval 34559

W3C validator