Nuprl Lemma : poset_anti_sym

[s:POSet{i}]. ∀[a,b:|s|].  (a b ∈ |s|) supposing ((b ≤ a) and (a ≤ b))


Definitions occuring in Statement :  poset: POSet{i} set_leq: a ≤ b set_car: |p| uimplies: supposing a uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uanti_sym: UniformlyAntiSym(T;x,y.R[x; y]) uimplies: supposing a prop: poset: POSet{i} qoset: QOSet dset: DSet
Lemmas referenced :  poset_properties set_leq_wf set_car_wf poset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule isect_memberEquality axiomEquality setElimination rename equalityTransitivity equalitySymmetry

\mforall{}[s:POSet\{i\}].  \mforall{}[a,b:|s|].    (a  =  b)  supposing  ((b  \mleq{}  a)  and  (a  \mleq{}  b))

Date html generated: 2016_05_15-PM-00_05_05
Last ObjectModification: 2015_12_26-PM-11_27_51

Theory : sets_1

Home Index