Nuprl Lemma : qoset_trans

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


Proof




Definitions occuring in Statement :  qoset: QOSet set_leq: a ≤ b set_car: |p| uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T upreorder: UniformPreorder(T;x,y.R[x; y]) and: P ∧ Q utrans: UniformlyTrans(T;x,y.E[x; y]) urefl: UniformlyRefl(T;x,y.E[x; y]) implies:  Q set_leq: a ≤ b infix_ap: y qoset: QOSet dset: DSet prop: uimplies: supposing a guard: {T}
Lemmas referenced :  qoset_properties assert_witness set_le_wf set_leq_wf set_car_wf qoset_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination sqequalRule isect_memberEquality lambdaEquality dependent_functionElimination applyEquality setElimination rename independent_functionElimination because_Cache equalityTransitivity equalitySymmetry

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



Date html generated: 2016_05_15-PM-00_04_38
Last ObjectModification: 2015_12_26-PM-11_28_29

Theory : sets_1


Home Index