### Nuprl Lemma : set_leq_weakening_lt

`∀[s:QOSet]. ∀[a,b:|s|].  a ≤ b supposing a <s b`

Proof

Definitions occuring in Statement :  qoset: `QOSet` set_lt: `a <p b` set_leq: `a ≤ b` set_car: `|p|` uimplies: `b supposing a` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` set_leq: `a ≤ b` infix_ap: `x f y` qoset: `QOSet` dset: `DSet` implies: `P `` Q` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q` strict_part: `strict_part(x,y.R[x; y];a;b)`
Lemmas referenced :  assert_witness set_le_wf set_lt_wf set_car_wf qoset_wf set_lt_is_sp_of_leq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution extract_by_obid isectElimination thin applyEquality setElimination rename hypothesisEquality hypothesis independent_functionElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry productElimination independent_isectElimination

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

Date html generated: 2019_10_15-AM-10_32_28
Last ObjectModification: 2018_08_22-AM-09_39_18

Theory : sets_1

Home Index