Definition df-mfs 33358

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 33338	. 2 class mFS
2		vt	. . . . . . . . 9 setvar 𝑡
3	2	cv 1538	. . . . . . . 8 class 𝑡
4		cmcn 33322	. . . . . . . 8 class mCN
5	3, 4	cfv 6418	. . . . . . 7 class (mCN‘𝑡)
6		cmvar 33323	. . . . . . . 8 class mVR
7	3, 6	cfv 6418	. . . . . . 7 class (mVR‘𝑡)
8	5, 7	cin 3882	. . . . . 6 class ((mCN‘𝑡) ∩ (mVR‘𝑡))
9		c0 4253	. . . . . 6 class ∅
10	8, 9	wceq 1539	. . . . 5 wff ((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅
11		cmtc 33326	. . . . . . 7 class mTC
12	3, 11	cfv 6418	. . . . . 6 class (mTC‘𝑡)
13		cmty 33324	. . . . . . 7 class mType
14	3, 13	cfv 6418	. . . . . 6 class (mType‘𝑡)
15	7, 12, 14	wf 6414	. . . . 5 wff (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)
16	10, 15	wa 395	. . . 4 wff (((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡))
17		cmax 33327	. . . . . . 7 class mAx
18	3, 17	cfv 6418	. . . . . 6 class (mAx‘𝑡)
19		cmsta 33337	. . . . . . 7 class mStat
20	3, 19	cfv 6418	. . . . . 6 class (mStat‘𝑡)
21	18, 20	wss 3883	. . . . 5 wff (mAx‘𝑡) ⊆ (mStat‘𝑡)
22	14	ccnv 5579	. . . . . . . . 9 class ◡(mType‘𝑡)
23		vv	. . . . . . . . . . 11 setvar 𝑣
24	23	cv 1538	. . . . . . . . . 10 class 𝑣
25	24	csn 4558	. . . . . . . . 9 class {𝑣}
26	22, 25	cima 5583	. . . . . . . 8 class (◡(mType‘𝑡) “ {𝑣})
27		cfn 8691	. . . . . . . 8 class Fin
28	26, 27	wcel 2108	. . . . . . 7 wff (◡(mType‘𝑡) “ {𝑣}) ∈ Fin
29	28	wn 3	. . . . . 6 wff ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin
30		cmvt 33325	. . . . . . 7 class mVT
31	3, 30	cfv 6418	. . . . . 6 class (mVT‘𝑡)
32	29, 23, 31	wral 3063	. . . . 5 wff ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin
33	21, 32	wa 395	. . . 4 wff ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin)
34	16, 33	wa 395	. . 3 wff ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))
35	34, 2	cab 2715	. 2 class {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))}
36	1, 35	wceq 1539	1 wff mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))}

This definition is referenced by:  ismfs  33411