Nuprl Lemma : setmem-setimages-2
∀A,b,x:coSet{i:l}. ((A ∈ setimages(b;x)) ⇐⇒ setimage{i:l}(A;b) ∧ (A ⊆ x))
Proof
Definitions occuring in Statement :
setimage: setimage{i:l}(x;b),
setimages: setimages(A;B),
setsubset: (a ⊆ b),
setmem: (x ∈ s),
coSet: coSet{i:l},
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
exists: ∃x:A. B[x],
function-graph: function-graph{i:l}(A;a.B[a];grph),
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
rev_implies: P ⇐ Q,
pi1: fst(t),
cand: A c∧ B,
guard: {T},
squash: ↓T,
true: True
Lemmas referenced :
function-graph_wf,
setmem_wf,
seteq_wf,
orderedpair-snd_wf,
pi1_wf,
coSet_wf,
set-image_wf,
setsubset_wf,
setmem-setimages,
setimage-iff,
setimages_wf,
setimage_wf,
orderedpairset_wf,
setmem_functionality_1,
orderedpairset_functionality,
seteq_weakening,
co-seteq-iff,
setmem-image,
seteq_functionality,
setsubset-iff,
sigmaset_wf,
setmem-sigmaset,
orderedpair-snd_functionality,
snd-orderedpairset,
seteq_inversion,
squash_wf,
true_wf,
fun-graph_wf,
setsubset_functionality,
function-graph-fun-graph,
setmem-fun-graph,
setmem_functionality
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
independent_pairFormation,
sqequalHypSubstitution,
productElimination,
thin,
sqequalRule,
productIsType,
because_Cache,
universeIsType,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
lambdaEquality_alt,
setIsType,
inhabitedIsType,
hypothesis,
functionIsType,
instantiate,
cumulativity,
applyEquality,
independent_functionElimination,
dependent_functionElimination,
promote_hyp,
independent_pairEquality,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_pairFormation_alt,
rename,
functionExtensionality,
productEquality,
dependent_pairEquality_alt,
hyp_replacement,
imageElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
dependent_set_memberEquality_alt,
applyLambdaEquality,
setElimination
Latex:
\mforall{}A,b,x:coSet\{i:l\}. ((A \mmember{} setimages(b;x)) \mLeftarrow{}{}\mRightarrow{} setimage\{i:l\}(A;b) \mwedge{} (A \msubseteq{} x))
Date html generated:
2020_05_20-PM-01_19_39
Last ObjectModification:
2020_01_06-PM-01_24_06
Theory : constructive!set!theory
Home
Index