Nuprl Lemma : extend-type-equiv

[T:Type]. EquivRel(Base;x,y.(x ∈ ⇐⇒ y ∈ T) ∧ ((x ∈ T)  (x y ∈ T)))


Proof




Definitions occuring in Statement :  equiv_rel: EquivRel(T;x,y.E[x; y]) uall: [x:A]. B[x] iff: ⇐⇒ Q implies:  Q and: P ∧ Q member: t ∈ T base: Base universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T equiv_rel: EquivRel(T;x,y.E[x; y]) and: P ∧ Q refl: Refl(T;x,y.E[x; y]) all: x:A. B[x] cand: c∧ B iff: ⇐⇒ Q implies:  Q rev_implies:  Q sym: Sym(T;x,y.E[x; y]) trans: Trans(T;x,y.E[x; y])
Lemmas referenced :  istype-base istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut independent_pairFormation Error :lambdaFormation_alt,  sqequalHypSubstitution equalityTransitivity hypothesis equalitySymmetry sqequalRule Error :equalityIstype,  Error :universeIsType,  hypothesisEquality sqequalBase because_Cache productElimination thin extract_by_obid independent_functionElimination Error :productIsType,  Error :functionIsType,  independent_pairEquality Error :lambdaEquality_alt,  dependent_functionElimination axiomEquality Error :functionIsTypeImplies,  Error :inhabitedIsType,  instantiate isectElimination universeEquality

Latex:
\mforall{}[T:Type].  EquivRel(Base;x,y.(x  \mmember{}  T  \mLeftarrow{}{}\mRightarrow{}  y  \mmember{}  T)  \mwedge{}  ((x  \mmember{}  T)  {}\mRightarrow{}  (x  =  y)))



Date html generated: 2019_06_20-PM-00_33_20
Last ObjectModification: 2018_11_25-PM-06_36_28

Theory : quot_1


Home Index