Metamath Proof Explorer

Definition df-mfs

Description: Define the set of all formal systems. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mfs 
|- mFS = { t | ( ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) ) /\ ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfs 
 |-  mFS
1 vt 
 |-  t
2 cmcn 
 |-  mCN
3 1 cv 
 |-  t
4 3 2 cfv 
 |-  ( mCN ` t )
5 cmvar 
 |-  mVR
6 3 5 cfv 
 |-  ( mVR ` t )
7 4 6 cin 
 |-  ( ( mCN ` t ) i^i ( mVR ` t ) )
8 c0 
 |-  (/)
9 7 8 wceq 
 |-  ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/)
10 cmty 
 |-  mType
11 3 10 cfv 
 |-  ( mType ` t )
12 cmtc 
 |-  mTC
13 3 12 cfv 
 |-  ( mTC ` t )
14 6 13 11 wf 
 |-  ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t )
15 9 14 wa 
 |-  ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) )
16 cmax 
 |-  mAx
17 3 16 cfv 
 |-  ( mAx ` t )
18 cmsta 
 |-  mStat
19 3 18 cfv 
 |-  ( mStat ` t )
20 17 19 wss 
 |-  ( mAx ` t ) C_ ( mStat ` t )
21 vv 
 |-  v
22 cmvt 
 |-  mVT
23 3 22 cfv 
 |-  ( mVT ` t )
24 11 ccnv 
 |-  `' ( mType ` t )
25 21 cv 
 |-  v
26 25 csn 
 |-  { v }
27 24 26 cima 
 |-  ( `' ( mType ` t ) " { v } )
28 cfn 
 |-  Fin
29 27 28 wcel 
 |-  ( `' ( mType ` t ) " { v } ) e. Fin
30 29 wn 
 |-  -. ( `' ( mType ` t ) " { v } ) e. Fin
31 30 21 23 wral 
 |-  A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin
32 20 31 wa 
 |-  ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin )
33 15 32 wa 
 |-  ( ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) ) /\ ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin ) )
34 33 1 cab 
 |-  { t | ( ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) ) /\ ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin ) ) }
35 0 34 wceq 
 |-  mFS = { t | ( ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) ) /\ ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin ) ) }