Nuprl Lemma : fset-ac-lub_wf

[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
  (fset-ac-lub(eq;ac1;ac2) ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )


Proof




Definitions occuring in Statement :  fset-ac-lub: fset-ac-lub(eq;ac1;ac2) fset-antichain: fset-antichain(eq;ac) fset: fset(T) deq: EqDecider(T) assert: b uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T fset-ac-lub: fset-ac-lub(eq;ac1;ac2) all: x:A. B[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  fset-minimals-antichain fset-union_wf fset_wf deq-fset_wf fset-minimals_wf f-proper-subset-dec_wf assert_wf fset-antichain_wf set_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality dependent_functionElimination hypothesis dependent_set_memberEquality lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[ac1,ac2:\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ].
    (fset-ac-lub(eq;ac1;ac2)  \mmember{}  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  )



Date html generated: 2016_05_14-PM-03_48_47
Last ObjectModification: 2015_12_26-PM-06_36_17

Theory : finite!sets


Home Index