Nuprl Lemma : qoset_lt_trans

[s:QOSet]. ∀[a,b,c:|s|].  (a <c) supposing ((b <c) and (a <b))


Definitions occuring in Statement :  qoset: QOSet set_lt: a <b set_car: |p| uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  utrans: UniformlyTrans(T;x,y.E[x; y]) uall: [x:A]. B[x] member: t ∈ T qoset: QOSet dset: DSet so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] implies:  Q iff: ⇐⇒ Q and: P ∧ Q strict_part: strict_part(x,y.R[x; y];a;b) set_leq: a ≤ b infix_ap: y not: ¬A false: False prop: rev_implies:  Q set_lt: a <b uimplies: supposing a guard: {T}
Lemmas referenced :  utrans_functionality_wrt_iff set_car_wf set_lt_wf strict_part_wf set_leq_wf iff_weakening_uiff set_lt_is_sp_of_leq assert_witness set_le_wf set_blt_wf qoset_wf utrans_imp_sp_utrans set_leq_trans
Rules used in proof :  cut sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis lambdaEquality because_Cache independent_functionElimination productElimination independent_pairEquality dependent_functionElimination applyEquality isect_memberEquality voidElimination equalityTransitivity equalitySymmetry

\mforall{}[s:QOSet].  \mforall{}[a,b,c:|s|].    (a  <s  c)  supposing  ((b  <s  c)  and  (a  <s  b))

Date html generated: 2016_05_15-PM-00_04_45
Last ObjectModification: 2015_12_26-PM-11_28_26

Theory : sets_1

Home Index