Nuprl Lemma : seteqtrans1

s1,s2,s3:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s3)  seteq(s1;s3))


Proof




Definitions occuring in Statement :  seteq: seteq(s1;s2) coSet: coSet{i:l} all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  trans: Trans(T;x,y.E[x; y]) guard: {T} uall: [x:A]. B[x] prop: member: t ∈ T implies:  Q all: x:A. B[x] and: P ∧ Q equiv_rel: EquivRel(T;x,y.E[x; y])
Lemmas referenced :  coSet_wf seteq_wf seteq-equiv
Rules used in proof :  independent_functionElimination dependent_functionElimination hypothesis hypothesisEquality isectElimination lambdaFormation thin productElimination sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution sqequalHypSubstitution extract_by_obid introduction cut

Latex:
\mforall{}s1,s2,s3:coSet\{i:l\}.    (seteq(s1;s2)  {}\mRightarrow{}  seteq(s2;s3)  {}\mRightarrow{}  seteq(s1;s3))



Date html generated: 2018_07_29-AM-09_51_13
Last ObjectModification: 2018_07_11-PM-00_09_07

Theory : constructive!set!theory


Home Index