Definition df-msa 31493

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

Assertion

Ref	Expression
df-msa	|- mSA = ( t e. _V |-> { a e. (mEx ` t ) | ( (m0St ` a ) e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` (mVR ` t ) ) ) } )

Distinct variable group:   t, a

Detailed syntax breakdown of Definition df-msa

Step	Hyp	Ref	Expression
1		cmsa 31483	. 2 class mSA
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		va	. . . . . . . 8 setvar a
5	4	cv 1482	. . . . . . 7 class a
6		cm0s 31482	. . . . . . 7 class m0St
7	5, 6	cfv 5888	. . . . . 6 class (m0St ` a )
8	2	cv 1482	. . . . . . 7 class t
9		cmax 31362	. . . . . . 7 class mAx
10	8, 9	cfv 5888	. . . . . 6 class (mAx ` t )
11	7, 10	wcel 1990	. . . . 5 wff (m0St ` a ) e. (mAx ` t )
12		c1st 7166	. . . . . . 7 class 1st
13	5, 12	cfv 5888	. . . . . 6 class ( 1st ` a )
14		cmvt 31360	. . . . . . 7 class mVT
15	8, 14	cfv 5888	. . . . . 6 class (mVT ` t )
16	13, 15	wcel 1990	. . . . 5 wff ( 1st ` a ) e. (mVT ` t )
17		c2nd 7167	. . . . . . . . 9 class 2nd
18	5, 17	cfv 5888	. . . . . . . 8 class ( 2nd ` a )
19	18	ccnv 5113	. . . . . . 7 class `' ( 2nd ` a )
20		cmvar 31358	. . . . . . . 8 class mVR
21	8, 20	cfv 5888	. . . . . . 7 class (mVR ` t )
22	19, 21	cres 5116	. . . . . 6 class ( `' ( 2nd ` a ) |` (mVR ` t ) )
23	22	wfun 5882	. . . . 5 wff Fun ( `' ( 2nd ` a ) |` (mVR ` t ) )
24	11, 16, 23	w3a 1037	. . . 4 wff ( (m0St ` a ) e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` (mVR ` t ) ) )
25		cmex 31364	. . . . 5 class mEx
26	8, 25	cfv 5888	. . . 4 class (mEx ` t )
27	24, 4, 26	crab 2916	. . 3 class { a e. (mEx ` t ) | ( (m0St ` a ) e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` (mVR ` t ) ) ) }
28	2, 3, 27	cmpt 4729	. 2 class ( t e. _V |-> { a e. (mEx ` t ) | ( (m0St ` a ) e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` (mVR ` t ) ) ) } )
29	1, 28	wceq 1483	1 wff mSA = ( t e. _V |-> { a e. (mEx ` t ) | ( (m0St ` a ) e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` (mVR ` t ) ) ) } )

This definition is referenced by: (None)