Nuprl Lemma : bar-wf-base

[T:Type]. bar(T) ∈ Type supposing T ⊆Base


Proof




Definitions occuring in Statement :  bar: bar(T) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] member: t ∈ T base: Base universe: Type
Definitions unfolded in proof :  bar: bar(T) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a
Lemmas referenced :  base_wf subtype_rel_wf partial_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  bar(T)  \mmember{}  Type  supposing  T  \msubseteq{}r  Base



Date html generated: 2016_05_15-PM-10_03_41
Last ObjectModification: 2016_01_05-PM-06_24_33

Theory : bar!type


Home Index