Nuprl Lemma : subset-co-regext
∀a:coSet{i:l}. (transitive-set(a) ⇒ (a ⊆ co-regext(a)))
Proof
Definitions occuring in Statement :
co-regext: co-regext(a),
transitive-set: transitive-set(s),
setsubset: (a ⊆ b),
coSet: coSet{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
prop: ℙ,
pi2: snd(t),
pi1: fst(t),
coW-dom: coW-dom(a.B[a];w),
coW-item: coW-item(w;b),
coWmem: coWmem(a.B[a];z;w),
mk-coset: mk-coset(T;f),
setmem: (x ∈ s),
co-regext: co-regext(a),
subtype_rel: A ⊆r B,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
so_apply: x[s],
so_lambda: λ2x.t[x],
seteq: seteq(s1;s2),
setsubset: (a ⊆ b),
set-dom: set-dom(s),
set-item: set-item(s;x),
allsetmem: ∀a∈A.P[a],
transitive-set: transitive-set(s),
coW-equiv: coW-equiv(a.B[a];w;w'),
coSet: coSet{i:l},
coW-game: coW-game(a.B[a];w;w'),
sg-pos: Pos(g),
nat: ℕ,
sg-init: InitialPos(g),
cand: A c∧ B,
copath-at: copath-at(w;p),
copath-nil: (),
coPath-at: coPath-at(n;w;p),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
btrue: tt,
regextfun: regextfun(f;w),
regextW: regextW(G;t),
Wsup: Wsup(a;b),
mk-set: f"(T),
sq_stable: SqStable(P),
squash: ↓T,
sg-legal1: Legal1(x;y),
sg-legal2: Legal2(x;y),
or: P ∨ Q,
uimplies: b supposing a,
decidable: Dec(P),
false: False,
guard: {T},
ge: i ≥ j ,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
top: Top,
true: True
Lemmas referenced :
transitive-set_wf,
coSet_wf,
setmem_wf,
coSet_subtype,
subtype_coSet,
co-regext_wf,
setsubset-iff,
all_wf,
set-item_wf,
seteq_wf,
exists_wf,
set-dom_wf,
subtype_rel_self,
equal_wf,
regextfun_wf,
regextW_wf,
seteq_functionality,
seteq_weakening,
good-sg-win2,
coW-game_wf,
coW_wf,
copath-length_wf,
nat_wf,
copath-at_wf,
sg-pos_wf,
sg-init_wf,
sg-legal1_wf,
sg-legal2_wf,
copath_length_nil_lemma,
copath-nil_wf,
pi1_wf,
copath_wf,
pi2_wf,
set_wf,
sq-stable-coW-game-legal1,
copath-last_wf,
decidable__lt,
nat_properties,
full-omega-unsat,
intformand_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
intformnot_wf,
intformless_wf,
intformeq_wf,
itermAdd_wf,
int_formula_prop_and_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_not_lemma,
int_formula_prop_less_lemma,
int_formula_prop_eq_lemma,
int_term_value_add_lemma,
int_formula_prop_wf,
copathAgree-last,
coW-dom_wf,
subtype_rel-equal,
squash_wf,
true_wf,
iff_weakening_equal,
coW-equiv_weakening,
coW-item_wf,
coW-equiv_wf,
co-seteq-iff,
mk-coset_wf,
copath-extend_wf,
copathAgree_wf,
length-copath-extend,
add_functionality_wrt_eq,
or_wf,
copathAgree-extend,
seteq_transitivity,
copath-at-extend,
seteq_inversion,
item_mk_set_lemma,
set-item-mem,
setmem_functionality_1,
decidable__equal_int
Rules used in proof :
rename,
sqequalRule,
applyEquality,
hypothesis_subsumption,
independent_functionElimination,
productElimination,
hypothesis,
isectElimination,
hypothesisEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
lambdaEquality,
because_Cache,
promote_hyp,
dependent_pairFormation,
functionExtensionality,
functionEquality,
equalityTransitivity,
equalitySymmetry,
universeEquality,
instantiate,
cumulativity,
productEquality,
intEquality,
setElimination,
independent_pairFormation,
setEquality,
natural_numberEquality,
imageMemberEquality,
baseClosed,
imageElimination,
unionElimination,
independent_isectElimination,
applyLambdaEquality,
approximateComputation,
int_eqEquality,
isect_memberEquality,
voidElimination,
voidEquality,
dependent_set_memberEquality,
independent_pairEquality,
inrFormation,
addEquality,
equalityUniverse,
levelHypothesis,
spreadEquality,
hyp_replacement,
inlFormation
Latex:
\mforall{}a:coSet\{i:l\}. (transitive-set(a) {}\mRightarrow{} (a \msubseteq{} co-regext(a)))
Date html generated:
2019_10_31-AM-06_34_45
Last ObjectModification:
2018_08_07-PM-01_43_56
Theory : constructive!set!theory
Home
Index