Nuprl Lemma : subset-regext
∀a:Set{i:l}. (transitive-set(a) ⇒ (a ⊆ regext(a)))
Proof
Definitions occuring in Statement :
regext: regext(a),
transitive-set: transitive-set(s),
setsubset: (a ⊆ b),
Set: Set{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
onto-map: R:(A ─>> B),
cand: A c∧ B,
allsetmem: ∀a∈A.P[a],
setsubset: (a ⊆ b),
top: Top,
mv-map: R:(A ⇒ B),
guard: {T},
set-relation: SetRelation(R),
exists: ∃x:A. B[x],
pi2: snd(t),
pi1: fst(t),
set-dom: set-dom(s),
set-item: set-item(s;x),
Wsup: Wsup(a;b),
mk-set: f"(T),
so_apply: x[s],
prop: ℙ,
so_lambda: λ2x.t[x],
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
seteq-iff-setsubset,
setmem_functionality_1,
item_mk_set_lemma,
dom_mk_set_lemma,
setmem-mk-set-sq,
setmem_functionality,
setsubset_functionality,
setmem-mk-set,
transitive-set-iff,
seteq_transitivity,
seteq_inversion,
seteq_weakening,
set-dom_wf,
exists_wf,
equal_wf,
seteq_wf,
regext-lemma,
transitive-set_wf,
all_wf,
mk-set_wf,
setmem-iff,
set-subtype,
subtype-set,
Set_wf,
setmem_wf,
set-induction,
set-subtype-coSet,
regext_wf,
setsubset-iff2
Rules used in proof :
productEquality,
independent_pairFormation,
voidEquality,
voidElimination,
isect_memberEquality,
equalitySymmetry,
equalityTransitivity,
instantiate,
dependent_pairFormation,
universeEquality,
rename,
hypothesis_subsumption,
because_Cache,
functionEquality,
cumulativity,
lambdaEquality,
independent_functionElimination,
productElimination,
sqequalRule,
applyEquality,
hypothesis,
isectElimination,
hypothesisEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}a:Set\{i:l\}. (transitive-set(a) {}\mRightarrow{} (a \msubseteq{} regext(a)))
Date html generated:
2018_07_29-AM-10_07_45
Last ObjectModification:
2018_07_20-PM-05_38_06
Theory : constructive!set!theory
Home
Index