Theorem mfsdisj

Description: The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mfsdisj.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
	mfsdisj.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
Assertion	mfsdisj	⊢ ( 𝑇 ∈ mFS → ( 𝐶 ∩ 𝑉 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mfsdisj.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
2		mfsdisj.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
3		eqid	⊢ ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 )
4		eqid	⊢ ( mVT ‘ 𝑇 ) = ( mVT ‘ 𝑇 )
5		eqid	⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
6		eqid	⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
7		eqid	⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 )
8	1 2 3 4 5 6 7	ismfs	⊢ ( 𝑇 ∈ mFS → ( 𝑇 ∈ mFS ↔ ( ( ( 𝐶 ∩ 𝑉 ) = ∅ ∧ ( mType ‘ 𝑇 ) : 𝑉 ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ◡ ( mType ‘ 𝑇 ) “ { 𝑣 } ) ∈ Fin ) ) ) )
9	8	ibi	⊢ ( 𝑇 ∈ mFS → ( ( ( 𝐶 ∩ 𝑉 ) = ∅ ∧ ( mType ‘ 𝑇 ) : 𝑉 ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ◡ ( mType ‘ 𝑇 ) “ { 𝑣 } ) ∈ Fin ) ) )
10	9	simplld	⊢ ( 𝑇 ∈ mFS → ( 𝐶 ∩ 𝑉 ) = ∅ )