Theorem ismfs

Description: A formal system is a tuple <. mCN , mVR , mType , mVT , mTC , mAx >. such that: mCN and mVR are disjoint; mType is a function from mVR to mVT ; mVT is a subset of mTC ; mAx is a set of statements; and for each variable typecode, there are infinitely many variables of that type. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	ismfs.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
	ismfs.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	ismfs.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
	ismfs.f	⊢ 𝐹 = ( mVT ‘ 𝑇 )
	ismfs.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
	ismfs.a	⊢ 𝐴 = ( mAx ‘ 𝑇 )
	ismfs.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
Assertion	ismfs	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑇 ∈ mFS ↔ ( ( ( 𝐶 ∩ 𝑉 ) = ∅ ∧ 𝑌 : 𝑉 ⟶ 𝐾 ) ∧ ( 𝐴 ⊆ 𝑆 ∧ ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismfs.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
2		ismfs.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
3		ismfs.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
4		ismfs.f	⊢ 𝐹 = ( mVT ‘ 𝑇 )
5		ismfs.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
6		ismfs.a	⊢ 𝐴 = ( mAx ‘ 𝑇 )
7		ismfs.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
8		fveq2	⊢ ( 𝑡 = 𝑇 → ( mCN ‘ 𝑡 ) = ( mCN ‘ 𝑇 ) )
9	8 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mCN ‘ 𝑡 ) = 𝐶 )
10		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = ( mVR ‘ 𝑇 ) )
11	10 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = 𝑉 )
12	9 11	ineq12d	⊢ ( 𝑡 = 𝑇 → ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ( 𝐶 ∩ 𝑉 ) )
13	12	eqeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ↔ ( 𝐶 ∩ 𝑉 ) = ∅ ) )
14		fveq2	⊢ ( 𝑡 = 𝑇 → ( mType ‘ 𝑡 ) = ( mType ‘ 𝑇 ) )
15	14 3	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mType ‘ 𝑡 ) = 𝑌 )
16		fveq2	⊢ ( 𝑡 = 𝑇 → ( mTC ‘ 𝑡 ) = ( mTC ‘ 𝑇 ) )
17	16 5	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mTC ‘ 𝑡 ) = 𝐾 )
18	15 11 17	feq123d	⊢ ( 𝑡 = 𝑇 → ( ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) ↔ 𝑌 : 𝑉 ⟶ 𝐾 ) )
19	13 18	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ∧ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) ) ↔ ( ( 𝐶 ∩ 𝑉 ) = ∅ ∧ 𝑌 : 𝑉 ⟶ 𝐾 ) ) )
20		fveq2	⊢ ( 𝑡 = 𝑇 → ( mAx ‘ 𝑡 ) = ( mAx ‘ 𝑇 ) )
21	20 6	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mAx ‘ 𝑡 ) = 𝐴 )
22		fveq2	⊢ ( 𝑡 = 𝑇 → ( mStat ‘ 𝑡 ) = ( mStat ‘ 𝑇 ) )
23	22 7	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mStat ‘ 𝑡 ) = 𝑆 )
24	21 23	sseq12d	⊢ ( 𝑡 = 𝑇 → ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ↔ 𝐴 ⊆ 𝑆 ) )
25		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVT ‘ 𝑡 ) = ( mVT ‘ 𝑇 ) )
26	25 4	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVT ‘ 𝑡 ) = 𝐹 )
27	15	cnveqd	⊢ ( 𝑡 = 𝑇 → ◡ ( mType ‘ 𝑡 ) = ◡ 𝑌 )
28	27	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) = ( ◡ 𝑌 “ { 𝑣 } ) )
29	28	eleq1d	⊢ ( 𝑡 = 𝑇 → ( ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ↔ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) )
30	29	notbid	⊢ ( 𝑡 = 𝑇 → ( ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ↔ ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) )
31	26 30	raleqbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ↔ ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) )
32	24 31	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ) ↔ ( 𝐴 ⊆ 𝑆 ∧ ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) )
33	19 32	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ∧ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) ) ∧ ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ) ) ↔ ( ( ( 𝐶 ∩ 𝑉 ) = ∅ ∧ 𝑌 : 𝑉 ⟶ 𝐾 ) ∧ ( 𝐴 ⊆ 𝑆 ∧ ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) ) )
34		df-mfs	⊢ mFS = { 𝑡 ∣ ( ( ( ( mCN ‘ 𝑡 ) ∩ ( mVR ‘ 𝑡 ) ) = ∅ ∧ ( mType ‘ 𝑡 ) : ( mVR ‘ 𝑡 ) ⟶ ( mTC ‘ 𝑡 ) ) ∧ ( ( mAx ‘ 𝑡 ) ⊆ ( mStat ‘ 𝑡 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑡 ) ¬ ( ◡ ( mType ‘ 𝑡 ) “ { 𝑣 } ) ∈ Fin ) ) }
35	33 34	elab2g	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑇 ∈ mFS ↔ ( ( ( 𝐶 ∩ 𝑉 ) = ∅ ∧ 𝑌 : 𝑉 ⟶ 𝐾 ) ∧ ( 𝐴 ⊆ 𝑆 ∧ ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) ) )