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 34435
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 6879 . . . . . . 7 (𝑡 = 𝑇 → (mCN‘𝑡) = (mCN‘𝑇))
2 ismfs.c . . . . . . 7 𝐶 = (mCN‘𝑇)
31, 2eqtr4di 2790 . . . . . 6 (𝑡 = 𝑇 → (mCN‘𝑡) = 𝐶)
4 fveq2 6879 . . . . . . 7 (𝑡 = 𝑇 → (mVR‘𝑡) = (mVR‘𝑇))
5 ismfs.v . . . . . . 7 𝑉 = (mVR‘𝑇)
64, 5eqtr4di 2790 . . . . . 6 (𝑡 = 𝑇 → (mVR‘𝑡) = 𝑉)
73, 6ineq12d 4210 . . . . 5 (𝑡 = 𝑇 → ((mCN‘𝑡) ∩ (mVR‘𝑡)) = (𝐶𝑉))
87eqeq1d 2734 . . . 4 (𝑡 = 𝑇 → (((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ↔ (𝐶𝑉) = ∅))
9 fveq2 6879 . . . . . 6 (𝑡 = 𝑇 → (mType‘𝑡) = (mType‘𝑇))
10 ismfs.y . . . . . 6 𝑌 = (mType‘𝑇)
119, 10eqtr4di 2790 . . . . 5 (𝑡 = 𝑇 → (mType‘𝑡) = 𝑌)
12 fveq2 6879 . . . . . 6 (𝑡 = 𝑇 → (mTC‘𝑡) = (mTC‘𝑇))
13 ismfs.k . . . . . 6 𝐾 = (mTC‘𝑇)
1412, 13eqtr4di 2790 . . . . 5 (𝑡 = 𝑇 → (mTC‘𝑡) = 𝐾)
1511, 6, 14feq123d 6694 . . . 4 (𝑡 = 𝑇 → ((mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡) ↔ 𝑌:𝑉𝐾))
168, 15anbi12d 631 . . 3 (𝑡 = 𝑇 → ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ↔ ((𝐶𝑉) = ∅ ∧ 𝑌:𝑉𝐾)))
17 fveq2 6879 . . . . . 6 (𝑡 = 𝑇 → (mAx‘𝑡) = (mAx‘𝑇))
18 ismfs.a . . . . . 6 𝐴 = (mAx‘𝑇)
1917, 18eqtr4di 2790 . . . . 5 (𝑡 = 𝑇 → (mAx‘𝑡) = 𝐴)
20 fveq2 6879 . . . . . 6 (𝑡 = 𝑇 → (mStat‘𝑡) = (mStat‘𝑇))
21 ismfs.s . . . . . 6 𝑆 = (mStat‘𝑇)
2220, 21eqtr4di 2790 . . . . 5 (𝑡 = 𝑇 → (mStat‘𝑡) = 𝑆)
2319, 22sseq12d 4012 . . . 4 (𝑡 = 𝑇 → ((mAx‘𝑡) ⊆ (mStat‘𝑡) ↔ 𝐴𝑆))
24 fveq2 6879 . . . . . 6 (𝑡 = 𝑇 → (mVT‘𝑡) = (mVT‘𝑇))
25 ismfs.f . . . . . 6 𝐹 = (mVT‘𝑇)
2624, 25eqtr4di 2790 . . . . 5 (𝑡 = 𝑇 → (mVT‘𝑡) = 𝐹)
2711cnveqd 5868 . . . . . . . 8 (𝑡 = 𝑇(mType‘𝑡) = 𝑌)
2827imaeq1d 6049 . . . . . . 7 (𝑡 = 𝑇 → ((mType‘𝑡) “ {𝑣}) = (𝑌 “ {𝑣}))
2928eleq1d 2818 . . . . . 6 (𝑡 = 𝑇 → (((mType‘𝑡) “ {𝑣}) ∈ Fin ↔ (𝑌 “ {𝑣}) ∈ Fin))
3029notbid 317 . . . . 5 (𝑡 = 𝑇 → (¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin ↔ ¬ (𝑌 “ {𝑣}) ∈ Fin))
3126, 30raleqbidv 3342 . . . 4 (𝑡 = 𝑇 → (∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin ↔ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin))
3223, 31anbi12d 631 . . 3 (𝑡 = 𝑇 → (((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin) ↔ (𝐴𝑆 ∧ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin)))
3316, 32anbi12d 631 . 2 (𝑡 = 𝑇 → (((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin)) ↔ (((𝐶𝑉) = ∅ ∧ 𝑌:𝑉𝐾) ∧ (𝐴𝑆 ∧ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin))))
34 df-mfs 34382 . 2 mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))}
3533, 34elab2g 3667 1 (𝑇𝑊 → (𝑇 ∈ mFS ↔ (((𝐶𝑉) = ∅ ∧ 𝑌:𝑉𝐾) ∧ (𝐴𝑆 ∧ ∀𝑣𝐹 ¬ (𝑌 “ {𝑣}) ∈ Fin))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  cin 3944  wss 3945  c0 4319  {csn 4623  ccnv 5669  cima 5673  wf 6529  cfv 6533  Fincfn 8924  mCNcmcn 34346  mVRcmvar 34347  mTypecmty 34348  mVTcmvt 34349  mTCcmtc 34350  mAxcmax 34351  mStatcmsta 34361  mFScmfs 34362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-mfs 34382
This theorem is referenced by:  mfsdisj  34436  mtyf2  34437  maxsta  34440  mvtinf  34441
  Copyright terms: Public domain W3C validator