Metamath Proof Explorer

Definition df-msa

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

Ref Expression
Assertion 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsa 
 |-  mSA
1 vt 
 |-  t
2 cvv 
 |-  _V
3 va 
 |-  a
4 cmex 
 |-  mEx
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mEx ` t )
7 cm0s 
 |-  m0St
8 3 cv 
 |-  a
9 8 7 cfv 
 |-  ( m0St ` a )
10 cmax 
 |-  mAx
11 5 10 cfv 
 |-  ( mAx ` t )
12 9 11 wcel 
 |-  ( m0St ` a ) e. ( mAx ` t )
13 c1st 
 |-  1st
14 8 13 cfv 
 |-  ( 1st ` a )
15 cmvt 
 |-  mVT
16 5 15 cfv 
 |-  ( mVT ` t )
17 14 16 wcel 
 |-  ( 1st ` a ) e. ( mVT ` t )
18 c2nd 
 |-  2nd
19 8 18 cfv 
 |-  ( 2nd ` a )
20 19 ccnv 
 |-  `' ( 2nd ` a )
21 cmvar 
 |-  mVR
22 5 21 cfv 
 |-  ( mVR ` t )
23 20 22 cres 
 |-  ( `' ( 2nd ` a ) |` ( mVR ` t ) )
24 23 wfun 
 |-  Fun ( `' ( 2nd ` a ) |` ( mVR ` t ) )
25 12 17 24 w3a 
 |-  ( ( m0St ` a ) e. ( mAx ` t ) /\ ( 1st ` a ) e. ( mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` ( mVR ` t ) ) )
26 25 3 6 crab 
 |-  { a e. ( mEx ` t ) | ( ( m0St ` a ) e. ( mAx ` t ) /\ ( 1st ` a ) e. ( mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` ( mVR ` t ) ) ) }
27 1 2 26 cmpt 
 |-  ( t e. _V |-> { a e. ( mEx ` t ) | ( ( m0St ` a ) e. ( mAx ` t ) /\ ( 1st ` a ) e. ( mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` ( mVR ` t ) ) ) } )
28 0 27 wceq 
 |-  mSA = ( t e. _V |-> { a e. ( mEx ` t ) | ( ( m0St ` a ) e. ( mAx ` t ) /\ ( 1st ` a ) e. ( mVT ` t ) /\ Fun ( `' ( 2nd ` a ) |` ( mVR ` t ) ) ) } )