Definition df-msa 36541

Description: Define the set of syntax axioms. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-msa	⊢ mSA = (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})

Distinct variable group:   𝑡,𝑎

Detailed syntax breakdown of Definition df-msa

Step	Hyp	Ref	Expression
1		cmsa 36531	. 2 class mSA
2		vt	. . 3 setvar 𝑡
3		cvv 3454	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1569	. . . . . . 7 class 𝑎
6		cm0s 36530	. . . . . . 7 class m0St
7	5, 6	cfv 6561	. . . . . 6 class (m0St‘𝑎)
8	2	cv 1569	. . . . . . 7 class 𝑡
9		cmax 36410	. . . . . . 7 class mAx
10	8, 9	cfv 6561	. . . . . 6 class (mAx‘𝑡)
11	7, 10	wcel 2147	. . . . 5 wff (m0St‘𝑎) ∈ (mAx‘𝑡)
12		c1st 8026	. . . . . . 7 class 1st
13	5, 12	cfv 6561	. . . . . 6 class (1st ‘𝑎)
14		cmvt 36408	. . . . . . 7 class mVT
15	8, 14	cfv 6561	. . . . . 6 class (mVT‘𝑡)
16	13, 15	wcel 2147	. . . . 5 wff (1st ‘𝑎) ∈ (mVT‘𝑡)
17		c2nd 8027	. . . . . . . . 9 class 2nd
18	5, 17	cfv 6561	. . . . . . . 8 class (2nd ‘𝑎)
19	18	ccnv 5655	. . . . . . 7 class ◡(2nd ‘𝑎)
20		cmvar 36406	. . . . . . . 8 class mVR
21	8, 20	cfv 6561	. . . . . . 7 class (mVR‘𝑡)
22	19, 21	cres 5658	. . . . . 6 class (◡(2nd ‘𝑎) ↾ (mVR‘𝑡))
23	22	wfun 6555	. . . . 5 wff Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡))
24	11, 16, 23	w3a 1103	. . . 4 wff ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))
25		cmex 36412	. . . . 5 class mEx
26	8, 25	cfv 6561	. . . 4 class (mEx‘𝑡)
27	24, 4, 26	crab 3416	. . 3 class {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))}
28	2, 3, 27	cmpt 5190	. 2 class (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})
29	1, 28	wceq 1570	1 wff mSA = (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})

This definition is used by: (None)