Nuprl Lemma : set_leq_antisymmetry
∀[s:POSet{i}]. ∀[a,b:|s|]. (a = b ∈ |s|) supposing ((b ≤ a) and (a ≤ b))
Proof
Definitions occuring in Statement :
poset: POSet{i},
set_leq: a ≤ b,
set_car: |p|,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uanti_sym: UniformlyAntiSym(T;x,y.R[x; y]),
uimplies: b 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
Latex:
\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_07
Last ObjectModification:
2015_12_26-PM-11_27_53
Theory : sets_1
Home
Index