Nuprl Lemma : least-closed-set-inductively-defined
∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']
∀B:Set{i:l}. ∀G:Set{i:l} ⟶ Set{i:l}.
((∀x,a:Set{i:l}. (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
⇒ (∀x,z:Set{i:l}. ((z ∈ G x) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z])))
⇒ inductively-defined{i:l}(x,a.R[x;a];least-closed-set(B;G)))
Proof
Definitions occuring in Statement :
least-closed-set: least-closed-set(B;G),
inductively-defined: inductively-defined{i:l}(x,a.R[x; a];s),
setimage: setimage{i:l}(x;b),
setsubset: (a ⊆ b),
Set: Set{i:l},
setmem: (x ∈ s),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
so_lambda: λ2x y.t[x; y],
mv-map: R:(A ⇒ B),
pi1: fst(t),
set-relation: SetRelation(R),
Regularset: Regular(A),
itersetfun: itersetfun(s.G[s];a),
uimplies: b supposing a,
set-function: set-function{i:l}(s; x.f[x]),
setimage: setimage{i:l}(x;b),
guard: {T},
relclosed-set: closed(x,a.R[x; a])s,
inductively-defined: inductively-defined{i:l}(x,a.R[x; a];s),
least-closed-set: least-closed-set(B;G),
so_apply: x[s],
so_lambda: λ2x.t[x],
so_apply: x[s1;s2],
cand: A c∧ B,
prop: ℙ,
exists: ∃x:A. B[x],
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
subtype_rel: A ⊆r B,
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x]
Lemmas referenced :
itersetfun-subset-fixpoint,
relclosed-set_wf,
setmem_functionality,
seteq_inversion,
setmem_functionality_1,
setunionfun_wf2,
itersetfun_functionality,
coSet-mem-Set-implies-Set,
seteq_functionality,
setmem-setunionfun,
seteq_wf,
seteq_weakening,
setsubset-iff,
coSet_wf,
coSet-subtype-Set,
itersetfun_wf,
setunionfun_wf,
equal_wf,
Regularset_wf,
regext_wf2,
setTC-transitive,
subset-regext,
setTC-contains,
regext_wf,
regext-Regularset,
setimage_wf,
subtype_rel_self,
iff_wf,
all_wf,
setmem_wf,
Set_wf,
exists_wf,
setsubset_wf,
set-subtype-coSet,
setsubset_transitivity,
setsubset-iff2
Rules used in proof :
setElimination,
independent_isectElimination,
functionExtensionality,
dependent_pairEquality,
rename,
setEquality,
equalitySymmetry,
equalityTransitivity,
universeEquality,
functionEquality,
impliesFunctionality,
allFunctionality,
addLevel,
lambdaEquality,
instantiate,
isectElimination,
cumulativity,
productEquality,
promote_hyp,
independent_pairFormation,
dependent_pairFormation,
independent_functionElimination,
productElimination,
sqequalRule,
because_Cache,
hypothesis,
hypothesisEquality,
applyEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[R:Set\{i:l\} {}\mrightarrow{} Set\{i:l\} {}\mrightarrow{} \mBbbP{}']
\mforall{}B:Set\{i:l\}. \mforall{}G:Set\{i:l\} {}\mrightarrow{} Set\{i:l\}.
((\mforall{}x,a:Set\{i:l\}. (R[x;a] {}\mRightarrow{} (\mexists{}b:Set\{i:l\}. ((b \mmember{} B) \mwedge{} setimage\{i:l\}(x;b)))))
{}\mRightarrow{} (\mforall{}x,z:Set\{i:l\}. ((z \mmember{} G x) \mLeftarrow{}{}\mRightarrow{} \mexists{}A:Set\{i:l\}. ((A \msubseteq{} x) \mwedge{} R[A;z])))
{}\mRightarrow{} inductively-defined\{i:l\}(x,a.R[x;a];least-closed-set(B;G)))
Date html generated:
2018_07_29-AM-10_09_54
Last ObjectModification:
2018_07_20-PM-01_27_24
Theory : constructive!set!theory
Home
Index