Nuprl Lemma : set-is-image
∀[A:Type]. ∀[B:A ⟶ Type]. {a:A| B[a]} ≡ Image((a:A × B[a]),(λp.(fst(p))))
Proof
Definitions occuring in Statement :
ext-eq: A ≡ B,
uall: ∀[x:A]. B[x],
so_apply: x[s],
pi1: fst(t),
image-type: Image(T,f),
set: {x:A| B[x]} ,
lambda: λx.A[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
so_apply: x[s],
subtype_rel: A ⊆r B,
and: P ∧ Q,
ext-eq: A ≡ B,
member: t ∈ T,
uall: ∀[x:A]. B[x],
pi1: fst(t)
Lemmas referenced :
image-type_wf
Rules used in proof :
because_Cache,
isect_memberEquality,
universeEquality,
cumulativity,
functionEquality,
axiomEquality,
independent_pairEquality,
productElimination,
sqequalRule,
hypothesis,
baseClosed,
productEquality,
thin,
isectElimination,
sqequalHypSubstitution,
lemma_by_obid,
applyEquality,
hypothesisEquality,
setEquality,
lambdaEquality,
independent_pairFormation,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
rename,
setElimination,
imageMemberEquality,
Error :dependent_pairEquality_alt,
Error :universeIsType,
imageElimination,
dependent_set_memberEquality
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \{a:A| B[a]\} \mequiv{} Image((a:A \mtimes{} B[a]),(\mlambda{}p.(fst(p))))
Date html generated:
2019_06_20-AM-11_19_32
Last ObjectModification:
2018_10_16-PM-02_50_01
Theory : subtype_0
Home
Index