Nuprl Lemma : comb_for_rng_mssum_wf

λs,r,f,a,z. Σx ∈ a. f[x] ∈ s:DSet ⟶ r:Rng ⟶ f:(|s| ⟶ |r|) ⟶ a:MSet{s} ⟶ (↓True) ⟶ |r|


Proof




Definitions occuring in Statement :  rng_mssum: rng_mssum mset: MSet{s} so_apply: x[s] squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] rng: Rng rng_car: |r| dset: DSet set_car: |p|
Definitions unfolded in proof :  member: t ∈ T squash: T all: x:A. B[x] uall: [x:A]. B[x] prop: dset: DSet rng: Rng
Lemmas referenced :  rng_mssum_wf squash_wf true_wf mset_wf set_car_wf rng_car_wf rng_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid dependent_functionElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry isectElimination functionEquality setElimination rename

Latex:
\mlambda{}s,r,f,a,z.  \mSigma{}x  \mmember{}  a.  f[x]  \mmember{}  s:DSet  {}\mrightarrow{}  r:Rng  {}\mrightarrow{}  f:(|s|  {}\mrightarrow{}  |r|)  {}\mrightarrow{}  a:MSet\{s\}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  |r|



Date html generated: 2016_05_16-AM-08_11_50
Last ObjectModification: 2015_12_28-PM-06_06_13

Theory : list_3


Home Index