Definition df-msa 35564

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 35554	. 2 class mSA
2		vt	. . 3 setvar 𝑡
3		cvv 3459	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1539	. . . . . . 7 class 𝑎
6		cm0s 35553	. . . . . . 7 class m0St
7	5, 6	cfv 6530	. . . . . 6 class (m0St‘𝑎)
8	2	cv 1539	. . . . . . 7 class 𝑡
9		cmax 35433	. . . . . . 7 class mAx
10	8, 9	cfv 6530	. . . . . 6 class (mAx‘𝑡)
11	7, 10	wcel 2108	. . . . 5 wff (m0St‘𝑎) ∈ (mAx‘𝑡)
12		c1st 7984	. . . . . . 7 class 1st
13	5, 12	cfv 6530	. . . . . 6 class (1st ‘𝑎)
14		cmvt 35431	. . . . . . 7 class mVT
15	8, 14	cfv 6530	. . . . . 6 class (mVT‘𝑡)
16	13, 15	wcel 2108	. . . . 5 wff (1st ‘𝑎) ∈ (mVT‘𝑡)
17		c2nd 7985	. . . . . . . . 9 class 2nd
18	5, 17	cfv 6530	. . . . . . . 8 class (2nd ‘𝑎)
19	18	ccnv 5653	. . . . . . 7 class ◡(2nd ‘𝑎)
20		cmvar 35429	. . . . . . . 8 class mVR
21	8, 20	cfv 6530	. . . . . . 7 class (mVR‘𝑡)
22	19, 21	cres 5656	. . . . . 6 class (◡(2nd ‘𝑎) ↾ (mVR‘𝑡))
23	22	wfun 6524	. . . . 5 wff Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡))
24	11, 16, 23	w3a 1086	. . . 4 wff ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))
25		cmex 35435	. . . . 5 class mEx
26	8, 25	cfv 6530	. . . 4 class (mEx‘𝑡)
27	24, 4, 26	crab 3415	. . 3 class {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))}
28	2, 3, 27	cmpt 5201	. 2 class (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})
29	1, 28	wceq 1540	1 wff mSA = (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})

This definition is referenced by: (None)