Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismfs Structured version   Unicode version

Theorem ismfs 30183
 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 mCN
ismfs.v mVR
ismfs.y mType
ismfs.f mVT
ismfs.k mTC
ismfs.a mAx
ismfs.s mStat
Assertion
Ref Expression
ismfs mFS
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem ismfs
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fveq2 5878 . . . . . . 7 mCN mCN
2 ismfs.c . . . . . . 7 mCN
31, 2syl6eqr 2481 . . . . . 6 mCN
4 fveq2 5878 . . . . . . 7 mVR mVR
5 ismfs.v . . . . . . 7 mVR
64, 5syl6eqr 2481 . . . . . 6 mVR
73, 6ineq12d 3665 . . . . 5 mCN mVR
87eqeq1d 2424 . . . 4 mCN mVR
9 fveq2 5878 . . . . . 6 mType mType
10 ismfs.y . . . . . 6 mType
119, 10syl6eqr 2481 . . . . 5 mType
12 fveq2 5878 . . . . . 6 mTC mTC
13 ismfs.k . . . . . 6 mTC
1412, 13syl6eqr 2481 . . . . 5 mTC
1511, 6, 14feq123d 5733 . . . 4 mTypemVRmTC
168, 15anbi12d 715 . . 3 mCN mVR mTypemVRmTC
17 fveq2 5878 . . . . . 6 mAx mAx
18 ismfs.a . . . . . 6 mAx
1917, 18syl6eqr 2481 . . . . 5 mAx
20 fveq2 5878 . . . . . 6 mStat mStat
21 ismfs.s . . . . . 6 mStat
2220, 21syl6eqr 2481 . . . . 5 mStat
2319, 22sseq12d 3493 . . . 4 mAx mStat
24 fveq2 5878 . . . . . 6 mVT mVT
25 ismfs.f . . . . . 6 mVT
2624, 25syl6eqr 2481 . . . . 5 mVT
2711cnveqd 5026 . . . . . . . 8 mType
2827imaeq1d 5183 . . . . . . 7 mType
2928eleq1d 2491 . . . . . 6 mType
3029notbid 295 . . . . 5 mType
3126, 30raleqbidv 3039 . . . 4 mVT mType
3223, 31anbi12d 715 . . 3 mAx mStat mVT mType
3316, 32anbi12d 715 . 2 mCN mVR mTypemVRmTC mAx mStat mVT mType
34 df-mfs 30130 . 2 mFS mCN mVR mTypemVRmTC mAx mStat mVT mType
3533, 34elab2g 3220 1 mFS
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   wceq 1437   wcel 1868  wral 2775   cin 3435   wss 3436  c0 3761  csn 3996  ccnv 4849  cima 4853  wf 5594  cfv 5598  cfn 7574  mCNcmcn 30094  mVRcmvar 30095  mTypecmty 30096  mVTcmvt 30097  mTCcmtc 30098  mAxcmax 30099  mStatcmsta 30109  mFScmfs 30110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-fv 5606  df-mfs 30130 This theorem is referenced by:  mfsdisj  30184  mtyf2  30185  maxsta  30188  mvtinf  30189
 Copyright terms: Public domain W3C validator