Metamath Proof Explorer

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 
|- C = ( mCN ` T )
ismfs.v 
|- V = ( mVR ` T )
ismfs.y 
|- Y = ( mType ` T )
ismfs.f 
|- F = ( mVT ` T )
ismfs.k 
|- K = ( mTC ` T )
ismfs.a 
|- A = ( mAx ` T )
ismfs.s 
|- S = ( mStat ` T )
Assertion ismfs 
|- ( T e. W -> ( T e. mFS <-> ( ( ( C i^i V ) = (/) /\ Y : V --> K ) /\ ( A C_ S /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) ) )

Proof

Step Hyp Ref Expression
1 ismfs.c 
 |-  C = ( mCN ` T )
2 ismfs.v 
 |-  V = ( mVR ` T )
3 ismfs.y 
 |-  Y = ( mType ` T )
4 ismfs.f 
 |-  F = ( mVT ` T )
5 ismfs.k 
 |-  K = ( mTC ` T )
6 ismfs.a 
 |-  A = ( mAx ` T )
7 ismfs.s 
 |-  S = ( mStat ` T )
8 fveq2 
 |-  ( t = T -> ( mCN ` t ) = ( mCN ` T ) )
9 8 1 eqtr4di 
 |-  ( t = T -> ( mCN ` t ) = C )
10 fveq2 
 |-  ( t = T -> ( mVR ` t ) = ( mVR ` T ) )
11 10 2 eqtr4di 
 |-  ( t = T -> ( mVR ` t ) = V )
12 9 11 ineq12d 
 |-  ( t = T -> ( ( mCN ` t ) i^i ( mVR ` t ) ) = ( C i^i V ) )
13 12 eqeq1d 
 |-  ( t = T -> ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) <-> ( C i^i V ) = (/) ) )
14 fveq2 
 |-  ( t = T -> ( mType ` t ) = ( mType ` T ) )
15 14 3 eqtr4di 
 |-  ( t = T -> ( mType ` t ) = Y )
16 fveq2 
 |-  ( t = T -> ( mTC ` t ) = ( mTC ` T ) )
17 16 5 eqtr4di 
 |-  ( t = T -> ( mTC ` t ) = K )
18 15 11 17 feq123d 
 |-  ( t = T -> ( ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) <-> Y : V --> K ) )
19 13 18 anbi12d 
 |-  ( t = T -> ( ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) ) <-> ( ( C i^i V ) = (/) /\ Y : V --> K ) ) )
20 fveq2 
 |-  ( t = T -> ( mAx ` t ) = ( mAx ` T ) )
21 20 6 eqtr4di 
 |-  ( t = T -> ( mAx ` t ) = A )
22 fveq2 
 |-  ( t = T -> ( mStat ` t ) = ( mStat ` T ) )
23 22 7 eqtr4di 
 |-  ( t = T -> ( mStat ` t ) = S )
24 21 23 sseq12d 
 |-  ( t = T -> ( ( mAx ` t ) C_ ( mStat ` t ) <-> A C_ S ) )
25 fveq2 
 |-  ( t = T -> ( mVT ` t ) = ( mVT ` T ) )
26 25 4 eqtr4di 
 |-  ( t = T -> ( mVT ` t ) = F )
27 15 cnveqd 
 |-  ( t = T -> `' ( mType ` t ) = `' Y )
28 27 imaeq1d 
 |-  ( t = T -> ( `' ( mType ` t ) " { v } ) = ( `' Y " { v } ) )
29 28 eleq1d 
 |-  ( t = T -> ( ( `' ( mType ` t ) " { v } ) e. Fin <-> ( `' Y " { v } ) e. Fin ) )
30 29 notbid 
 |-  ( t = T -> ( -. ( `' ( mType ` t ) " { v } ) e. Fin <-> -. ( `' Y " { v } ) e. Fin ) )
31 26 30 raleqbidv 
 |-  ( t = T -> ( A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin <-> A. v e. F -. ( `' Y " { v } ) e. Fin ) )
32 24 31 anbi12d 
 |-  ( t = T -> ( ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin ) <-> ( A C_ S /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) )
33 19 32 anbi12d 
 |-  ( t = T -> ( ( ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) ) /\ ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin ) ) <-> ( ( ( C i^i V ) = (/) /\ Y : V --> K ) /\ ( A C_ S /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) ) )
34 df-mfs 
 |-  mFS = { t | ( ( ( ( mCN ` t ) i^i ( mVR ` t ) ) = (/) /\ ( mType ` t ) : ( mVR ` t ) --> ( mTC ` t ) ) /\ ( ( mAx ` t ) C_ ( mStat ` t ) /\ A. v e. ( mVT ` t ) -. ( `' ( mType ` t ) " { v } ) e. Fin ) ) }
35 33 34 elab2g 
 |-  ( T e. W -> ( T e. mFS <-> ( ( ( C i^i V ) = (/) /\ Y : V --> K ) /\ ( A C_ S /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) ) )