Nuprl Lemma : dep-isect-subtype2

[A1,A2:Type]. ∀[B1:A1 ⟶ Type]. ∀[B2:A2 ⟶ Type].
  (x:A1 ⋂ B1[x] ⊆x:A2 ⋂ B2[x]) supposing ((∀x:A1. (B1[x] ⊆B2[x])) and (A1 ⊆A2))


Proof




Definitions occuring in Statement :  dep-isect: x:A ⋂ B[x] 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
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B guard: {T} all: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] prop:
Lemmas referenced :  dep-isect-subtype subtype_rel_transitivity dep-isect_wf all_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality dependentIntersectionElimination sqequalHypSubstitution dependentIntersection_memberEquality hypothesisEquality applyEquality thin extract_by_obid dependent_functionElimination sqequalRule hypothesis instantiate isectElimination cumulativity independent_isectElimination equalityTransitivity equalitySymmetry axiomEquality isect_memberEquality because_Cache functionEquality universeEquality

Latex:
\mforall{}[A1,A2:Type].  \mforall{}[B1:A1  {}\mrightarrow{}  Type].  \mforall{}[B2:A2  {}\mrightarrow{}  Type].
    (x:A1  \mcap{}  B1[x]  \msubseteq{}r  x:A2  \mcap{}  B2[x])  supposing  ((\mforall{}x:A1.  (B1[x]  \msubseteq{}r  B2[x]))  and  (A1  \msubseteq{}r  A2))



Date html generated: 2018_07_25-PM-01_30_18
Last ObjectModification: 2018_06_09-PM-09_18_12

Theory : dependent!intersection


Home Index