Nuprl Lemma : isect_subtype

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


Proof




Definitions occuring in Statement :  uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] isect: 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 so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B prop: and: P ∧ Q
Lemmas referenced :  subtype_rel_isect_general all_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis universeEquality because_Cache independent_isectElimination independent_pairFormation axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality cumulativity

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



Date html generated: 2016_05_13-PM-04_10_39
Last ObjectModification: 2015_12_26-AM-11_21_56

Theory : subtype_1


Home Index