Definition df-mfs 31393

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

Assertion

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

Distinct variable group:   v, t

Detailed syntax breakdown of Definition df-mfs

Step	Hyp	Ref	Expression
1		cmfs 31373	. 2 class mFS
2		vt	. . . . . . . . 9 setvar t
3	2	cv 1482	. . . . . . . 8 class t
4		cmcn 31357	. . . . . . . 8 class mCN
5	3, 4	cfv 5888	. . . . . . 7 class (mCN ` t )
6		cmvar 31358	. . . . . . . 8 class mVR
7	3, 6	cfv 5888	. . . . . . 7 class (mVR ` t )
8	5, 7	cin 3573	. . . . . 6 class ( (mCN ` t ) i^i (mVR ` t ) )
9		c0 3915	. . . . . 6 class (/)
10	8, 9	wceq 1483	. . . . 5 wff ( (mCN ` t ) i^i (mVR ` t ) ) = (/)
11		cmtc 31361	. . . . . . 7 class mTC
12	3, 11	cfv 5888	. . . . . 6 class (mTC ` t )
13		cmty 31359	. . . . . . 7 class mType
14	3, 13	cfv 5888	. . . . . 6 class (mType ` t )
15	7, 12, 14	wf 5884	. . . . 5 wff (mType ` t ) : (mVR ` t ) --> (mTC ` t )
16	10, 15	wa 384	. . . 4 wff ( ( (mCN ` t ) i^i (mVR ` t ) ) = (/) /\ (mType ` t ) : (mVR ` t ) --> (mTC ` t ) )
17		cmax 31362	. . . . . . 7 class mAx
18	3, 17	cfv 5888	. . . . . 6 class (mAx ` t )
19		cmsta 31372	. . . . . . 7 class mStat
20	3, 19	cfv 5888	. . . . . 6 class (mStat ` t )
21	18, 20	wss 3574	. . . . 5 wff (mAx ` t ) C_ (mStat ` t )
22	14	ccnv 5113	. . . . . . . . 9 class `' (mType ` t )
23		vv	. . . . . . . . . . 11 setvar v
24	23	cv 1482	. . . . . . . . . 10 class v
25	24	csn 4177	. . . . . . . . 9 class { v }
26	22, 25	cima 5117	. . . . . . . 8 class ( `' (mType ` t ) " { v } )
27		cfn 7955	. . . . . . . 8 class Fin
28	26, 27	wcel 1990	. . . . . . 7 wff ( `' (mType ` t ) " { v } ) e. Fin
29	28	wn 3	. . . . . 6 wff -. ( `' (mType ` t ) " { v } ) e. Fin
30		cmvt 31360	. . . . . . 7 class mVT
31	3, 30	cfv 5888	. . . . . 6 class (mVT ` t )
32	29, 23, 31	wral 2912	. . . . 5 wff A. v e. (mVT ` t ) -. ( `' (mType ` t ) " { v } ) e. Fin
33	21, 32	wa 384	. . . 4 wff ( (mAx ` t ) C_ (mStat ` t ) /\ A. v e. (mVT ` t ) -. ( `' (mType ` t ) " { v } ) e. Fin )
34	16, 33	wa 384	. . 3 wff ( ( ( (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	34, 2	cab 2608	. 2 class { 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 ) ) }
36	1, 35	wceq 1483	1 wff 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 ) ) }

This definition is referenced by:  ismfs  31446