Definition df-msa 34873

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 34863	. 2 class mSA
2		vt	. . 3 setvar 𝑡
3		cvv 3474	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1540	. . . . . . 7 class 𝑎
6		cm0s 34862	. . . . . . 7 class m0St
7	5, 6	cfv 6543	. . . . . 6 class (m0St‘𝑎)
8	2	cv 1540	. . . . . . 7 class 𝑡
9		cmax 34742	. . . . . . 7 class mAx
10	8, 9	cfv 6543	. . . . . 6 class (mAx‘𝑡)
11	7, 10	wcel 2106	. . . . 5 wff (m0St‘𝑎) ∈ (mAx‘𝑡)
12		c1st 7975	. . . . . . 7 class 1st
13	5, 12	cfv 6543	. . . . . 6 class (1st ‘𝑎)
14		cmvt 34740	. . . . . . 7 class mVT
15	8, 14	cfv 6543	. . . . . 6 class (mVT‘𝑡)
16	13, 15	wcel 2106	. . . . 5 wff (1st ‘𝑎) ∈ (mVT‘𝑡)
17		c2nd 7976	. . . . . . . . 9 class 2nd
18	5, 17	cfv 6543	. . . . . . . 8 class (2nd ‘𝑎)
19	18	ccnv 5675	. . . . . . 7 class ◡(2nd ‘𝑎)
20		cmvar 34738	. . . . . . . 8 class mVR
21	8, 20	cfv 6543	. . . . . . 7 class (mVR‘𝑡)
22	19, 21	cres 5678	. . . . . 6 class (◡(2nd ‘𝑎) ↾ (mVR‘𝑡))
23	22	wfun 6537	. . . . 5 wff Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡))
24	11, 16, 23	w3a 1087	. . . 4 wff ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))
25		cmex 34744	. . . . 5 class mEx
26	8, 25	cfv 6543	. . . 4 class (mEx‘𝑡)
27	24, 4, 26	crab 3432	. . 3 class {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))}
28	2, 3, 27	cmpt 5231	. 2 class (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})
29	1, 28	wceq 1541	1 wff mSA = (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})

This definition is referenced by: (None)