Nuprl Lemma : setmem-transmem
∀x,y:coSet{i:l}. ((x ∈ y) ⇒ (x ∈∈ y))
Proof
Definitions occuring in Statement :
transmem: (x ∈∈ y),
setmem: (x ∈ s),
coSet: coSet{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
rel_implies: R1 => R2,
infix_ap: x f y,
guard: {T},
prop: ℙ,
member: t ∈ T,
uall: ∀[x:A]. B[x],
transmem: (x ∈∈ y),
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
coSet_wf,
setmem_wf,
transitive-closure-contains
Rules used in proof :
independent_functionElimination,
dependent_functionElimination,
sqequalRule,
hypothesis,
hypothesisEquality,
cumulativity,
lambdaEquality,
because_Cache,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
instantiate,
thin,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}x,y:coSet\{i:l\}. ((x \mmember{} y) {}\mRightarrow{} (x \mmember{}\mmember{} y))
Date html generated:
2018_07_29-AM-10_03_24
Last ObjectModification:
2018_07_18-PM-11_37_00
Theory : constructive!set!theory
Home
Index