### Nuprl Lemma : qoset_lt_irrefl

`∀[s:QOSet]. ∀[a,b:|s|].  ¬(a = b ∈ |s|) supposing a <s b`

Proof

Definitions occuring in Statement :  qoset: `QOSet` set_lt: `a <p b` set_car: `|p|` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` qoset: `QOSet` dset: `DSet` uiff: `uiff(P;Q)` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  equal_wf set_car_wf set_lt_wf qoset_wf set_lt_is_sp_of_leq strict_part_irrefl set_leq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination extract_by_obid isectElimination setElimination rename hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination because_Cache isect_memberEquality equalityTransitivity equalitySymmetry productElimination independent_isectElimination

Latex:
\mforall{}[s:QOSet].  \mforall{}[a,b:|s|].    \mneg{}(a  =  b)  supposing  a  <s  b

Date html generated: 2017_10_01-AM-08_13_13
Last ObjectModification: 2017_02_28-PM-01_57_16

Theory : sets_1

Home Index