---

Step * of Lemma name-morph-flip-id

∀I:Cname List. ∀x:nameset(I). ∀c2:cat-ob(poset-cat(I)).  (c2 = flip(c2;x) ∈ cat-ob(poset-cat(I-[x])))
BY
{ (Auto THEN RepUR ``poset-cat cat-ob`` 0 THEN RepUR ``poset-cat cat-ob`` -1) }

1
1. I : Cname List
2. x : nameset(I)
3. c2 : name-morph(I;[])
⊢ c2 = flip(c2;x) ∈ name-morph(I-[x];[])

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}x:nameset(I).  \mforall{}c2:cat-ob(poset-cat(I)).    (c2  =  flip(c2;x))


By

---

Latex:
(Auto  THEN  RepUR  ``poset-cat  cat-ob``  0  THEN  RepUR  ``poset-cat  cat-ob``  -1)

---

Home Index