Nuprl Lemma : ftype_properties
∀s:DSet. ∀a:MSet{s}. ∀x:FTy{s}(a). (↑(x ∈b a))
Proof
Definitions occuring in Statement :
ftype: FTy{s}(a),
mset_mem: mset_mem,
mset: MSet{s},
assert: ↑b,
all: ∀x:A. B[x],
dset: DSet
Definitions unfolded in proof :
all: ∀x:A. B[x],
ftype: FTy{s}(a),
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
dset_wf,
mset_wf,
ftype_wf,
decidable__assert,
mset_mem_wf,
assert_wf,
sq_stable_from_decidable
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
setElimination,
thin,
rename,
cut,
lemma_by_obid,
isectElimination,
dependent_functionElimination,
hypothesisEquality,
hypothesis,
independent_functionElimination,
introduction,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
\mforall{}s:DSet. \mforall{}a:MSet\{s\}. \mforall{}x:FTy\{s\}(a). (\muparrow{}(x \mmember{}\msubb{} a))
Date html generated:
2016_05_16-AM-07_47_22
Last ObjectModification:
2016_01_16-PM-11_40_06
Theory : mset
Home
Index