Metamath Proof Explorer

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 
|- C = ( mCN ` T )
mfsdisj.v 
|- V = ( mVR ` T )
Assertion mfsdisj 
|- ( T e. mFS -> ( C i^i V ) = (/) )

Proof

Step Hyp Ref Expression
1 mfsdisj.c 
 |-  C = ( mCN ` T )
2 mfsdisj.v 
 |-  V = ( mVR ` T )
3 eqid 
 |-  ( mType ` T ) = ( mType ` T )
4 eqid 
 |-  ( mVT ` T ) = ( mVT ` T )
5 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
6 eqid 
 |-  ( mAx ` T ) = ( mAx ` T )
7 eqid 
 |-  ( mStat ` T ) = ( mStat ` T )
8 1 2 3 4 5 6 7 ismfs 
 |-  ( T e. mFS -> ( T e. mFS <-> ( ( ( C i^i V ) = (/) /\ ( mType ` T ) : V --> ( mTC ` T ) ) /\ ( ( mAx ` T ) C_ ( mStat ` T ) /\ A. v e. ( mVT ` T ) -. ( `' ( mType ` T ) " { v } ) e. Fin ) ) ) )
9 8 ibi 
 |-  ( T e. mFS -> ( ( ( C i^i V ) = (/) /\ ( mType ` T ) : V --> ( mTC ` T ) ) /\ ( ( mAx ` T ) C_ ( mStat ` T ) /\ A. v e. ( mVT ` T ) -. ( `' ( mType ` T ) " { v } ) e. Fin ) ) )
10 9 simplld 
 |-  ( T e. mFS -> ( C i^i V ) = (/) )