Nuprl Lemma : is-above-singleton-subtype
∀[A:Type]. ∀[a:A]. ∀[B:Type]. ∀[z:Base]. (is-above(A;a;z) ⇒ is-above(B;a;z)) supposing {x:A| x = a ∈ A} ⊆r B
Proof
Definitions occuring in Statement :
is-above: is-above(T;a;z),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
base: Base,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
subtype_rel: A ⊆r B,
implies: P ⇒ Q,
prop: ℙ,
is-above: is-above(T;a;z),
exists: ∃x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
squash: ↓T
Lemmas referenced :
is-above-subtype,
equal_wf,
is-above_wf,
istype-base,
subtype_rel_wf,
istype-universe,
istype-sqle
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
cut,
introduction,
sqequalRule,
axiomEquality,
hypothesis,
thin,
rename,
Error :lambdaFormation_alt,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
setEquality,
hypothesisEquality,
independent_isectElimination,
Error :dependent_set_memberEquality_alt,
Error :equalityIstype,
Error :inhabitedIsType,
independent_functionElimination,
Error :universeIsType,
instantiate,
universeEquality,
productElimination,
Error :dependent_pairFormation_alt,
because_Cache,
independent_pairFormation,
Error :productIsType,
Error :setIsType,
sqequalBase,
equalitySymmetry,
applyLambdaEquality,
setElimination,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
\mforall{}[A:Type]. \mforall{}[a:A]. \mforall{}[B:Type].
\mforall{}[z:Base]. (is-above(A;a;z) {}\mRightarrow{} is-above(B;a;z)) supposing \{x:A| x = a\} \msubseteq{}r B
Date html generated:
2019_06_20-PM-00_28_13
Last ObjectModification:
2019_01_20-PM-02_37_17
Theory : subtype_1
Home
Index