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