### Nuprl Lemma : b_all-wf2

`∀[T:Type]. ∀[b:bag(T)]. ∀[P:{x:T| x ↓∈ b}  ⟶ ℙ].  (b_all(T;b;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]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` b_all: `b_all(T;b;x.P[x])` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` so_apply: `x[s]` subtype_rel: `A ⊆r B`
Lemmas referenced :  all_wf bag-member_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality lambdaEquality functionEquality because_Cache hypothesis applyEquality dependent_set_memberEquality universeEquality axiomEquality equalityTransitivity equalitySymmetry setEquality isect_memberEquality

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

Date html generated: 2016_05_15-PM-02_41_15
Last ObjectModification: 2015_12_27-AM-09_40_50

Theory : bags

Home Index