### Nuprl Lemma : b_all-inst

`∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B.  (x ↓∈ b `` b_all(B;b;x.P[x]) `` P[x])`

Proof

Definitions occuring in Statement :  b_all: `b_all(T;b;x.P[x])` bag-member: `x ↓∈ bs` bag: `bag(T)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}` b_all: `b_all(T;b;x.P[x])`
Lemmas referenced :  b_all_wf bag-member_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis functionEquality cumulativity universeEquality dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[B:Type].  \mforall{}b:bag(B).  \mforall{}P:B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}x:B.    (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  b\_all(B;b;x.P[x])  {}\mRightarrow{}  P[x])

Date html generated: 2016_05_15-PM-02_41_26
Last ObjectModification: 2015_12_27-AM-09_40_46

Theory : bags

Home Index