Definition df-mfs 30647

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

Assertion

Ref	Expression
df-mfs	⊢ mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))}

Distinct variable group:   𝑣,𝑡

Detailed syntax breakdown of Definition df-mfs

Step	Hyp	Ref	Expression
1		cmfs 30627	. 2 class mFS
2		vt	. . . . . . . . 9 setvar 𝑡
3	2	cv 1474	. . . . . . . 8 class 𝑡
4		cmcn 30611	. . . . . . . 8 class mCN
5	3, 4	cfv 5804	. . . . . . 7 class (mCN‘𝑡)
6		cmvar 30612	. . . . . . . 8 class mVR
7	3, 6	cfv 5804	. . . . . . 7 class (mVR‘𝑡)
8	5, 7	cin 3539	. . . . . 6 class ((mCN‘𝑡) ∩ (mVR‘𝑡))
9		c0 3874	. . . . . 6 class ∅
10	8, 9	wceq 1475	. . . . 5 wff ((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅
11		cmtc 30615	. . . . . . 7 class mTC
12	3, 11	cfv 5804	. . . . . 6 class (mTC‘𝑡)
13		cmty 30613	. . . . . . 7 class mType
14	3, 13	cfv 5804	. . . . . 6 class (mType‘𝑡)
15	7, 12, 14	wf 5800	. . . . 5 wff (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)
16	10, 15	wa 383	. . . 4 wff (((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡))
17		cmax 30616	. . . . . . 7 class mAx
18	3, 17	cfv 5804	. . . . . 6 class (mAx‘𝑡)
19		cmsta 30626	. . . . . . 7 class mStat
20	3, 19	cfv 5804	. . . . . 6 class (mStat‘𝑡)
21	18, 20	wss 3540	. . . . 5 wff (mAx‘𝑡) ⊆ (mStat‘𝑡)
22	14	ccnv 5037	. . . . . . . . 9 class ◡(mType‘𝑡)
23		vv	. . . . . . . . . . 11 setvar 𝑣
24	23	cv 1474	. . . . . . . . . 10 class 𝑣
25	24	csn 4125	. . . . . . . . 9 class {𝑣}
26	22, 25	cima 5041	. . . . . . . 8 class (◡(mType‘𝑡) “ {𝑣})
27		cfn 7841	. . . . . . . 8 class Fin
28	26, 27	wcel 1977	. . . . . . 7 wff (◡(mType‘𝑡) “ {𝑣}) ∈ Fin
29	28	wn 3	. . . . . 6 wff ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin
30		cmvt 30614	. . . . . . 7 class mVT
31	3, 30	cfv 5804	. . . . . 6 class (mVT‘𝑡)
32	29, 23, 31	wral 2896	. . . . 5 wff ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin
33	21, 32	wa 383	. . . 4 wff ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin)
34	16, 33	wa 383	. . 3 wff ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))
35	34, 2	cab 2596	. 2 class {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))}
36	1, 35	wceq 1475	1 wff mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))}

This definition is referenced by:  ismfs  30700