---

Step * of Lemma set-eq_wf

∀[s,s':coSet{i:l}].  (set-eq(s;s') ∈ ℙ)
BY
{ (ProveWfLemma
   THEN GenConcl ⌜νR.λs,s'. ((∀i:set-dom(s). ∃j:set-dom(s'). (R set-item(s;i) set-item(s';j)))
                           ∧ (∀j:set-dom(s'). ∃i:set-dom(s). (R set-item(s;i) set-item(s';j))))
                  = P
                  ∈ (coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s,s':coSet\{i:l\}].    (set-eq(s;s')  \mmember{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma
  THEN  GenConcl  \mkleeneopen{}\mnu{}R.\mlambda{}s,s'.  ((\mforall{}i:set-dom(s).  \mexists{}j:set-dom(s').  (R  set-item(s;i)  set-item(s';j)))
                                                  \mwedge{}  (\mforall{}j:set-dom(s').  \mexists{}i:set-dom(s).  (R  set-item(s;i)  set-item(s';j))))
                                =  P\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index