Nuprl Lemma : subtype_rel_dep_function_iff

[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (uiff(∀[a:C]. (B[a] ⊆D[a]);(a:A ⟶ B[a]) ⊆(c:C ⟶ D[c]))) supposing 
     ((∀x,y:A.  Dec(x y ∈ A)) and 
     (a:A ⟶ B[a]) and 
     (C ⊆A))


Definitions occuring in Statement :  decidable: Dec(P) uiff: uiff(P;Q) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] subtype_rel: A ⊆B prop: exists: x:A. B[x] implies:  Q decidable: Dec(P) or: P ∨ Q assert: b ifthenelse: if then else fi  btrue: tt iff: ⇐⇒ Q true: True rev_implies:  Q bfalse: ff not: ¬A false: False bool: 𝔹 unit: Unit it: squash: T guard: {T} sq_type: SQType(T) bnot: ¬bb
Lemmas referenced :  subtype_rel_dep_function istype-universe subtype_rel_wf decidable_wf equal_wf subtype_rel_self true_wf false_wf assert_wf equal-wf-T-base bool_wf bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot subtype_rel-equal squash_wf iff_weakening_equal bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :lambdaEquality_alt,  applyEquality hypothesis independent_isectElimination Error :lambdaFormation_alt,  axiomEquality Error :isectIsType,  Error :universeIsType,  because_Cache Error :isect_memberEquality_alt,  functionEquality productElimination independent_pairEquality equalityTransitivity equalitySymmetry Error :functionIsType,  Error :inhabitedIsType,  universeEquality rename Error :dependent_pairFormation_alt,  Error :equalityIsType1,  dependent_functionElimination independent_functionElimination functionExtensionality unionElimination natural_numberEquality voidElimination Error :productIsType,  baseClosed equalityElimination instantiate imageElimination imageMemberEquality promote_hyp cumulativity

\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].
    (uiff(\mforall{}[a:C].  (B[a]  \msubseteq{}r  D[a]);(a:A  {}\mrightarrow{}  B[a])  \msubseteq{}r  (c:C  {}\mrightarrow{}  D[c])))  supposing 
          ((\mforall{}x,y:A.    Dec(x  =  y))  and 
          (a:A  {}\mrightarrow{}  B[a])  and 
          (C  \msubseteq{}r  A))

Date html generated: 2019_06_20-PM-00_27_37
Last ObjectModification: 2018_10_06-AM-11_20_16

Theory : subtype_1

Home Index