Nuprl Lemma : setmemfunclemma_ext
∀x1,s1,x2,s2:coSet{i:l}. (seteq(x1;x2) ⇒ seteq(s1;s2) ⇒ {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})
Proof
Definitions occuring in Statement :
setmem: (x ∈ s),
seteq: seteq(s1;s2),
coSet: coSet{i:l},
guard: {T},
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q
Definitions unfolded in proof :
seq-nil: seq-nil(),
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
squash: ↓T,
guard: {T},
prop: ℙ,
has-value: (a)↓,
all: ∀x:A. B[x],
strict4: strict4(F),
uimplies: b supposing a,
so_apply: x[s1;s2;s3;s4],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
uall: ∀[x:A]. B[x],
any: any x,
bool_cases,
isom-games_inversion,
win2strat-properties,
isom-preserves-win2,
coW-game-step-isom,
isom-win2,
coW-equiv_transitivity,
sq_stable__equal,
sq_stable__and,
win2-iff,
coW-equiv_inversion,
coW-equiv-implies,
coW-equiv-iff,
seteq_inversion,
seteq_transitivity,
co-seteq-iff,
setmem-iff,
setmemfunclemma,
set-item: set-item(s;x),
seq-comp: f o s,
seq-cons: seq-cons(a;s),
sg-init: InitialPos(g),
coPathAgree: coPathAgree(a.B[a];n;w;p;q),
copathAgree: copathAgree(a.B[a];w;x;y),
copath-length: copath-length(p),
or: P ∨ Q,
subtract: n - m,
pi2: snd(t),
coW-item: coW-item(w;b),
pi1: fst(t),
coW-dom: coW-dom(a.B[a];w),
top: Top,
btrue: tt,
ifthenelse: if b then t else f fi ,
coPath: coPath(a.B[a];w;n),
false: False,
true: True,
less_than': less_than'(a;b),
implies: P ⇒ Q,
not: ¬A,
and: P ∧ Q,
le: A ≤ B,
nat: ℕ,
copath: copath(a.B[a];w),
coW-game: coW-game(a.B[a];w;w'),
so_apply: x[s],
so_lambda: λ2x.t[x],
it: ⋅,
bfalse: ff,
eq_int: (i =z j),
member: t ∈ T
Lemmas referenced :
lifting-strict-decide,
strict4-decide,
lifting-strict-int_eq,
strict4-spread,
equal_wf,
top_wf,
is-exception_wf,
base_wf,
has-value_wf_base,
lifting-strict-spread,
setmemfunclemma,
bool_cases,
isom-games_inversion,
win2strat-properties,
isom-preserves-win2,
coW-game-step-isom,
isom-win2,
coW-equiv_transitivity,
sq_stable__equal,
sq_stable__and,
win2-iff,
coW-equiv_inversion,
coW-equiv-implies,
coW-equiv-iff,
seteq_inversion,
seteq_transitivity,
co-seteq-iff,
setmem-iff
Rules used in proof :
exceptionSqequal,
axiomSqleEquality,
spreadExceptionCases,
independent_functionElimination,
dependent_functionElimination,
sqleReflexivity,
productElimination,
productEquality,
callbyvalueSpread,
divergentSqle,
sqequalSqle,
because_Cache,
inlFormation,
imageElimination,
imageMemberEquality,
inrFormation,
applyExceptionCases,
hypothesisEquality,
closedConclusion,
baseApply,
callbyvalueApply,
lambdaFormation,
independent_pairFormation,
independent_isectElimination,
voidEquality,
voidElimination,
isect_memberEquality,
baseClosed,
isectElimination,
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}x1,s1,x2,s2:coSet\{i:l\}. (seteq(x1;x2) {}\mRightarrow{} seteq(s1;s2) {}\mRightarrow{} \{(x1 \mmember{} s1) \mLeftarrow{}{}\mRightarrow{} (x2 \mmember{} s2)\})
Date html generated:
2018_07_29-AM-09_51_31
Last ObjectModification:
2018_07_11-PM-00_32_26
Theory : constructive!set!theory
Home
Index