Nuprl Lemma : b_all-cons

`∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B.  ((∀b:B. SqStable(P[b])) `` (b_all(B;x.b;x.P[x]) `⇐⇒` P[x] ∧ b_all(B;b;x.P[x])))`

Proof

Definitions occuring in Statement :  b_all: `b_all(T;b;x.P[x])` cons-bag: `x.b` bag: `bag(T)` sq_stable: `SqStable(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `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` iff: `P `⇐⇒` Q` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` b_all: `b_all(T;b;x.P[x])` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` uimplies: `b supposing a` sq_or: `a ↓∨ b` or: `P ∨ Q` squash: `↓T` sq_stable: `SqStable(P)` guard: `{T}`
Lemmas referenced :  b_all_wf cons-bag_wf all_wf sq_stable_wf bag_wf bag-member-cons bag-member_wf sq_stable__bag-member equal_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality functionExtensionality productElimination productEquality universeEquality functionEquality dependent_functionElimination independent_functionElimination because_Cache independent_isectElimination inlFormation imageMemberEquality baseClosed inrFormation imageElimination unionElimination equalitySymmetry dependent_set_memberEquality setElimination rename setEquality hyp_replacement Error :applyLambdaEquality

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

Date html generated: 2016_10_25-AM-10_29_01
Last ObjectModification: 2016_07_12-AM-06_45_05

Theory : bags

Home Index