Nuprl Lemma : is-above-axiom
∀[z:Base]. z ~ Ax supposing is-above(Unit;Ax;z)
Proof
Definitions occuring in Statement :
is-above: is-above(T;a;z),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
unit: Unit,
base: Base,
sqequal: s ~ t,
axiom: Ax
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a
Lemmas referenced :
is-above-axiom-general,
unit_wf2,
unit_subtype_base
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
independent_isectElimination
Latex:
\mforall{}[z:Base]. z \msim{} Ax supposing is-above(Unit;Ax;z)
Date html generated:
2019_06_20-PM-00_28_17
Last ObjectModification:
2019_01_20-PM-02_28_23
Theory : subtype_1
Home
Index