Theorem ismfs 31446

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
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 ) ) ) )

Distinct variable groups:   v, F   v, T

Allowed substitution hints:   A( v)   C( v)   S( v)   K( v)   V( v)   W( v)   Y( v)

Proof of Theorem ismfs

Dummy variable t is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6191	. . . . . . 7 |- ( t = T -> (mCN ` t ) = (mCN ` T ) )
2		ismfs.c	. . . . . . 7 |- C = (mCN ` T )
3	1, 2	syl6eqr 2674	. . . . . 6 |- ( t = T -> (mCN ` t ) = C )
4		fveq2 6191	. . . . . . 7 |- ( t = T -> (mVR ` t ) = (mVR ` T ) )
5		ismfs.v	. . . . . . 7 |- V = (mVR ` T )
6	4, 5	syl6eqr 2674	. . . . . 6 |- ( t = T -> (mVR ` t ) = V )
7	3, 6	ineq12d 3815	. . . . 5 |- ( t = T -> ( (mCN ` t ) i^i (mVR ` t ) ) = ( C i^i V ) )
8	7	eqeq1d 2624	. . . 4 |- ( t = T -> ( ( (mCN ` t ) i^i (mVR ` t ) ) = (/) <-> ( C i^i V ) = (/) ) )
9		fveq2 6191	. . . . . 6 |- ( t = T -> (mType ` t ) = (mType ` T ) )
10		ismfs.y	. . . . . 6 |- Y = (mType ` T )
11	9, 10	syl6eqr 2674	. . . . 5 |- ( t = T -> (mType ` t ) = Y )
12		fveq2 6191	. . . . . 6 |- ( t = T -> (mTC ` t ) = (mTC ` T ) )
13		ismfs.k	. . . . . 6 |- K = (mTC ` T )
14	12, 13	syl6eqr 2674	. . . . 5 |- ( t = T -> (mTC ` t ) = K )
15	11, 6, 14	feq123d 6034	. . . 4 |- ( t = T -> ( (mType ` t ) : (mVR ` t ) --> (mTC ` t ) <-> Y : V --> K ) )
16	8, 15	anbi12d 747	. . 3 |- ( t = T -> ( ( ( (mCN ` t ) i^i (mVR ` t ) ) = (/) /\ (mType ` t ) : (mVR ` t ) --> (mTC ` t ) ) <-> ( ( C i^i V ) = (/) /\ Y : V --> K ) ) )
17		fveq2 6191	. . . . . 6 |- ( t = T -> (mAx ` t ) = (mAx ` T ) )
18		ismfs.a	. . . . . 6 |- A = (mAx ` T )
19	17, 18	syl6eqr 2674	. . . . 5 |- ( t = T -> (mAx ` t ) = A )
20		fveq2 6191	. . . . . 6 |- ( t = T -> (mStat ` t ) = (mStat ` T ) )
21		ismfs.s	. . . . . 6 |- S = (mStat ` T )
22	20, 21	syl6eqr 2674	. . . . 5 |- ( t = T -> (mStat ` t ) = S )
23	19, 22	sseq12d 3634	. . . 4 |- ( t = T -> ( (mAx ` t ) C_ (mStat ` t ) <-> A C_ S ) )
24		fveq2 6191	. . . . . 6 |- ( t = T -> (mVT ` t ) = (mVT ` T ) )
25		ismfs.f	. . . . . 6 |- F = (mVT ` T )
26	24, 25	syl6eqr 2674	. . . . 5 |- ( t = T -> (mVT ` t ) = F )
27	11	cnveqd 5298	. . . . . . . 8 |- ( t = T -> `' (mType ` t ) = `' Y )
28	27	imaeq1d 5465	. . . . . . 7 |- ( t = T -> ( `' (mType ` t ) " { v } ) = ( `' Y " { v } ) )
29	28	eleq1d 2686	. . . . . 6 |- ( t = T -> ( ( `' (mType ` t ) " { v } ) e. Fin <-> ( `' Y " { v } ) e. Fin ) )
30	29	notbid 308	. . . . 5 |- ( t = T -> ( -. ( `' (mType ` t ) " { v } ) e. Fin <-> -. ( `' Y " { v } ) e. Fin ) )
31	26, 30	raleqbidv 3152	. . . 4 |- ( t = T -> ( A. v e. (mVT ` t ) -. ( `' (mType ` t ) " { v } ) e. Fin <-> A. v e. F -. ( `' Y " { v } ) e. Fin ) )
32	23, 31	anbi12d 747	. . 3 |- ( 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	16, 32	anbi12d 747	. 2 |- ( 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 31393	. 2 |- 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 3353	1 |- ( T e. W -> ( T e. mFS <-> ( ( ( C i^i V ) = (/) /\ Y : V --> K ) /\ ( A C_ S /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   `'ccnv 5113   "cima 5117   -->wf 5884   ` cfv 5888   Fincfn 7955  mCNcmcn 31357  mVRcmvar 31358  mTypecmty 31359  mVTcmvt 31360  mTCcmtc 31361  mAxcmax 31362  mStatcmsta 31372  mFScmfs 31373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-mfs 31393

This theorem is referenced by:  mfsdisj  31447  mtyf2  31448  maxsta  31451  mvtinf  31452