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

Theorem ismfs 30506
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 ↔ (((𝐶𝑉) = ∅ ∧ 𝑌:𝑉𝐾) ∧ (𝐴𝑆 ∧ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin))))
Distinct variable groups:   𝑣,𝐹   𝑣,𝑇
Allowed substitution hints:   𝐴(𝑣)   𝐶(𝑣)   𝑆(𝑣)   𝐾(𝑣)   𝑉(𝑣)   𝑊(𝑣)   𝑌(𝑣)

Proof of Theorem ismfs
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6088 . . . . . . 7 (𝑡 = 𝑇 → (mCN‘𝑡) = (mCN‘𝑇))
2 ismfs.c . . . . . . 7 𝐶 = (mCN‘𝑇)
31, 2syl6eqr 2661 . . . . . 6 (𝑡 = 𝑇 → (mCN‘𝑡) = 𝐶)
4 fveq2 6088 . . . . . . 7 (𝑡 = 𝑇 → (mVR‘𝑡) = (mVR‘𝑇))
5 ismfs.v . . . . . . 7 𝑉 = (mVR‘𝑇)
64, 5syl6eqr 2661 . . . . . 6 (𝑡 = 𝑇 → (mVR‘𝑡) = 𝑉)
73, 6ineq12d 3776 . . . . 5 (𝑡 = 𝑇 → ((mCN‘𝑡) ∩ (mVR‘𝑡)) = (𝐶𝑉))
87eqeq1d 2611 . . . 4 (𝑡 = 𝑇 → (((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ↔ (𝐶𝑉) = ∅))
9 fveq2 6088 . . . . . 6 (𝑡 = 𝑇 → (mType‘𝑡) = (mType‘𝑇))
10 ismfs.y . . . . . 6 𝑌 = (mType‘𝑇)
119, 10syl6eqr 2661 . . . . 5 (𝑡 = 𝑇 → (mType‘𝑡) = 𝑌)
12 fveq2 6088 . . . . . 6 (𝑡 = 𝑇 → (mTC‘𝑡) = (mTC‘𝑇))
13 ismfs.k . . . . . 6 𝐾 = (mTC‘𝑇)
1412, 13syl6eqr 2661 . . . . 5 (𝑡 = 𝑇 → (mTC‘𝑡) = 𝐾)
1511, 6, 14feq123d 5933 . . . 4 (𝑡 = 𝑇 → ((mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡) ↔ 𝑌:𝑉𝐾))
168, 15anbi12d 742 . . 3 (𝑡 = 𝑇 → ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ↔ ((𝐶𝑉) = ∅ ∧ 𝑌:𝑉𝐾)))
17 fveq2 6088 . . . . . 6 (𝑡 = 𝑇 → (mAx‘𝑡) = (mAx‘𝑇))
18 ismfs.a . . . . . 6 𝐴 = (mAx‘𝑇)
1917, 18syl6eqr 2661 . . . . 5 (𝑡 = 𝑇 → (mAx‘𝑡) = 𝐴)
20 fveq2 6088 . . . . . 6 (𝑡 = 𝑇 → (mStat‘𝑡) = (mStat‘𝑇))
21 ismfs.s . . . . . 6 𝑆 = (mStat‘𝑇)
2220, 21syl6eqr 2661 . . . . 5 (𝑡 = 𝑇 → (mStat‘𝑡) = 𝑆)
2319, 22sseq12d 3596 . . . 4 (𝑡 = 𝑇 → ((mAx‘𝑡) ⊆ (mStat‘𝑡) ↔ 𝐴𝑆))
24 fveq2 6088 . . . . . 6 (𝑡 = 𝑇 → (mVT‘𝑡) = (mVT‘𝑇))
25 ismfs.f . . . . . 6 𝐹 = (mVT‘𝑇)
2624, 25syl6eqr 2661 . . . . 5 (𝑡 = 𝑇 → (mVT‘𝑡) = 𝐹)
2711cnveqd 5208 . . . . . . . 8 (𝑡 = 𝑇(mType‘𝑡) = 𝑌)
2827imaeq1d 5371 . . . . . . 7 (𝑡 = 𝑇 → ((mType‘𝑡) “ {𝑣}) = (𝑌 “ {𝑣}))
2928eleq1d 2671 . . . . . 6 (𝑡 = 𝑇 → (((mType‘𝑡) “ {𝑣}) ∈ Fin ↔ (𝑌 “ {𝑣}) ∈ Fin))
3029notbid 306 . . . . 5 (𝑡 = 𝑇 → (¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin ↔ ¬ (𝑌 “ {𝑣}) ∈ Fin))
3126, 30raleqbidv 3128 . . . 4 (𝑡 = 𝑇 → (∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin ↔ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin))
3223, 31anbi12d 742 . . 3 (𝑡 = 𝑇 → (((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin) ↔ (𝐴𝑆 ∧ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin)))
3316, 32anbi12d 742 . 2 (𝑡 = 𝑇 → (((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin)) ↔ (((𝐶𝑉) = ∅ ∧ 𝑌:𝑉𝐾) ∧ (𝐴𝑆 ∧ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin))))
34 df-mfs 30453 . 2 mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))}
3533, 34elab2g 3321 1 (𝑇𝑊 → (𝑇 ∈ mFS ↔ (((𝐶𝑉) = ∅ ∧ 𝑌:𝑉𝐾) ∧ (𝐴𝑆 ∧ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  cin 3538  wss 3539  c0 3873  {csn 4124  ccnv 5027  cima 5031  wf 5786  cfv 5790  Fincfn 7818  mCNcmcn 30417  mVRcmvar 30418  mTypecmty 30419  mVTcmvt 30420  mTCcmtc 30421  mAxcmax 30422  mStatcmsta 30432  mFScmfs 30433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-mfs 30453
This theorem is referenced by:  mfsdisj  30507  mtyf2  30508  maxsta  30511  mvtinf  30512
  Copyright terms: Public domain W3C validator