Nuprl Lemma : cosetTC-contained
∀s:coSet{i:l}. (transitive-set(s) ⇒ (cosetTC(s) ⊆ s))
Proof
Definitions occuring in Statement :
transitive-set: transitive-set(s),
setsubset: (a ⊆ b),
cosetTC: cosetTC(a),
coSet: coSet{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
prop: ℙ,
uall: ∀[x:A]. B[x]
Lemmas referenced :
cosetTC-least,
setsubset-iff,
setmem_wf,
coSet_wf,
transitive-set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
because_Cache,
independent_functionElimination,
productElimination,
hypothesis,
isectElimination,
hypothesisEquality
Latex:
\mforall{}s:coSet\{i:l\}. (transitive-set(s) {}\mRightarrow{} (cosetTC(s) \msubseteq{} s))
Date html generated:
2019_10_31-AM-06_33_54
Last ObjectModification:
2018_08_04-AM-10_25_56
Theory : constructive!set!theory
Home
Index