Nuprl Lemma : set_lt_transitivity_2

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


Proof




Definitions occuring in Statement :  qoset: QOSet set_lt: a <b 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 uimplies: supposing a qoset: QOSet dset: DSet uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) set_lt: a <b implies:  Q prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] set_leq: a ≤ b infix_ap: y guard: {T}
Lemmas referenced :  set_lt_is_sp_of_leq assert_witness set_blt_wf set_leq_wf set_lt_wf set_car_wf qoset_wf utrans_imp_sp_utrans_b set_le_wf set_leq_trans
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis productElimination independent_isectElimination sqequalRule independent_functionElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry lambdaEquality applyEquality

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



Date html generated: 2016_05_15-PM-00_04_56
Last ObjectModification: 2015_12_26-PM-11_28_05

Theory : sets_1


Home Index