### Nuprl Lemma : bag-member-map2

`∀[T,U:Type].  ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs}  ⟶ U.  uiff(x ↓∈ bag-map(f;bs);↓∃v:{v:T| v ↓∈ bs} . (x = (f v) ∈ U))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-map: `bag-map(f;bs)` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` squash: `↓T` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` bag-member: `x ↓∈ bs`
Lemmas referenced :  bag-member_wf bag-map-member-wf bag-member-map bag-subtype equal_wf squash_wf exists_wf bag-subtype2 iff_weakening_uiff bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache hypothesis setEquality dependent_functionElimination equalityTransitivity equalitySymmetry independent_pairFormation imageElimination productElimination setElimination rename dependent_pairFormation dependent_set_memberEquality applyEquality sqequalRule imageMemberEquality baseClosed universeIsType lambdaEquality productEquality independent_functionElimination independent_isectElimination functionIsType setIsType inhabitedIsType universeEquality

Latex:
\mforall{}[T,U:Type].
\mforall{}x:U.  \mforall{}bs:bag(T).  \mforall{}f:\{v:T|  v  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  U.
uiff(x  \mdownarrow{}\mmember{}  bag-map(f;bs);\mdownarrow{}\mexists{}v:\{v:T|  v  \mdownarrow{}\mmember{}  bs\}  .  (x  =  (f  v)))

Date html generated: 2019_10_15-AM-11_02_17
Last ObjectModification: 2018_09_27-AM-11_19_25

Theory : bags

Home Index