Definition df-mfs

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmfs	⊢ mFS
1		vt	⊢ 𝑡
2		cmcn	⊢ mCN
3	1	cv	⊢ 𝑡
4	3 2	cfv	⊢ ( mCN ‘ 𝑡 )
5		cmvar	⊢ mVR
6	3 5	cfv	⊢ ( mVR ‘ 𝑡 )
7	4 6	cin	⊢ ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) )
8		c0	⊢ ∅
9	7 8	wceq	⊢ ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅
10		cmty	⊢ mType
11	3 10	cfv	⊢ ( mType ‘ 𝑡 )
12		cmtc	⊢ mTC
13	3 12	cfv	⊢ ( mTC ‘ 𝑡 )
14	6 13 11	wf	⊢ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 )
15	9 14	wa	⊢ ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ∧ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) )
16		cmax	⊢ mAx
17	3 16	cfv	⊢ ( mAx ‘ 𝑡 )
18		cmsta	⊢ mStat
19	3 18	cfv	⊢ ( mStat ‘ 𝑡 )
20	17 19	wss	⊢ ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 )
21		vv	⊢ 𝑣
22		cmvt	⊢ mVT
23	3 22	cfv	⊢ ( mVT ‘ 𝑡 )
24	11	ccnv	⊢ ◡ ( mType ‘ 𝑡 )
25	21	cv	⊢ 𝑣
26	25	csn	⊢ { 𝑣 }
27	24 26	cima	⊢ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } )
28		cfn	⊢ Fin
29	27 28	wcel	⊢ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin
30	29	wn	⊢ ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin
31	30 21 23	wral	⊢ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin
32	20 31	wa	⊢ ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin )
33	15 32	wa	⊢ ( ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ∧ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) ) ∧ ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ) )
34	33 1	cab	⊢ { 𝑡 ∣ ( ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ∧ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) ) ∧ ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ) ) }
35	0 34	wceq	⊢ mFS = { 𝑡 ∣ ( ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ∧ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) ) ∧ ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ) ) }