Nuprl Lemma : is-above-pair

[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[b:B[a]].
  ∀z:Base. (is-above(a:A × B[a];<a, b>;z)  (∃c,d:Base. ((z ~ <c, d>) ∧ is-above(A;a;c) ∧ is-above(B[a];b;d))))


Proof




Definitions occuring in Statement :  is-above: is-above(T;a;z) uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q function: x:A ⟶ B[x] pair: <a, b> product: x:A × B[x] base: Base universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q exists: x:A. B[x] member: t ∈ T is-above: is-above(T;a;z) and: P ∧ Q subtype_rel: A ⊆B guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a top: Top pi2: snd(t) pi1: fst(t) has-value: (a)↓ or: P ∨ Q prop: cand: c∧ B istype: istype(T) false: False not: ¬A
Lemmas referenced :  pair-eta subtype_rel_product top_wf istype-top istype-void has-value-monotonic has-value_wf_base is-exception_wf has-value-implies-dec-ispair-2 is-above_wf base_wf sqle_wf_base subtype_rel-equal equal_functionality_wrt_subtype_rel2 not-btrue-sqle-bfalse
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :dependent_pairFormation_alt,  sqequalRule baseApply closedConclusion baseClosed hypothesisEquality sqequalHypSubstitution productElimination thin cut introduction extract_by_obid isectElimination equalityTransitivity hypothesis equalitySymmetry applyEquality Error :lambdaEquality_alt,  functionExtensionality cumulativity Error :inhabitedIsType,  independent_isectElimination Error :isect_memberEquality_alt,  voidElimination Error :universeIsType,  because_Cache applyLambdaEquality divergentSqle sqleReflexivity dependent_functionElimination independent_functionElimination unionElimination Error :productIsType,  sqequalIntensionalEquality productEquality Error :dependent_pairEquality_alt,  Error :functionIsType,  universeEquality independent_pairFormation Error :equalityIsType2,  sqleRule

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[a:A].  \mforall{}[b:B[a]].
    \mforall{}z:Base.  (is-above(a:A  \mtimes{}  B[a];<a,  b>z)  {}\mRightarrow{}  (\mexists{}c,d:Base.  ((z  \msim{}  <c,  d>)  \mwedge{}  is-above(A;a;c)  \mwedge{}  is-above(\000CB[a];b;d))))



Date html generated: 2019_06_20-PM-00_28_20
Last ObjectModification: 2018_09_29-PM-11_16_01

Theory : subtype_1


Home Index