---

Step * of Lemma fset-antichain-add

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(fset(T))]. ∀[x:fset(T)].
  uiff(↑fset-antichain(eq;fset-add(deq-fset(eq);x;s));(↑fset-antichain(eq;s))
  ∧ (∀xs:fset(T). (¬xs ⊆≠ x) ∧ (¬x ⊆≠ xs) supposing xs ∈ s))
BY
{ ((UnivCD THENA Auto) THEN RWW "assert-fset-antichain member-fset-add" 0 THEN Auto THEN SplitOrHyps THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(fset(T))].  \mforall{}[x:fset(T)].
    uiff(\muparrow{}fset-antichain(eq;fset-add(deq-fset(eq);x;s));(\muparrow{}fset-antichain(eq;s))
    \mwedge{}  (\mforall{}xs:fset(T).  (\mneg{}xs  \msubseteq{}\mneq{}  x)  \mwedge{}  (\mneg{}x  \msubseteq{}\mneq{}  xs)  supposing  xs  \mmember{}  s))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RWW  "assert-fset-antichain  member-fset-add"  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index