---

Step * 2 of Lemma poset-cat-arrow-filter-nil


1. I : Cname List
2. J : nameset(I) List
3. nameset(J) ⊆r nameset(I)
⊢ ∀c1,c2:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) c1 c2.
    ((filter(λz.(c1 z =z c2 z);J) = [] ∈ ({x:nameset(J)| ↑(c1 x =z c2 x)}  List))
    ⇒ (∀j∈J.((c1 j) = 0 ∈ ℕ2) ∧ ((c2 j) = 1 ∈ ℕ2)))
BY
{ Auto }

1
1. I : Cname List
2. J : nameset(I) List
3. nameset(J) ⊆r nameset(I)
4. c1 : cat-ob(poset-cat(I))
5. c2 : cat-ob(poset-cat(I))
6. f : cat-arrow(poset-cat(I)) c1 c2
7. filter(λz.(c1 z =z c2 z);J) = [] ∈ ({x:nameset(J)| ↑(c1 x =z c2 x)}  List)
⊢ (∀j∈J.((c1 j) = 0 ∈ ℕ2) ∧ ((c2 j) = 1 ∈ ℕ2))

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  nameset(I)  List
3.  nameset(J)  \msubseteq{}r  nameset(I)
\mvdash{}  \mforall{}c1,c2:cat-ob(poset-cat(I)).  \mforall{}f:cat-arrow(poset-cat(I))  c1  c2.
        ((filter(\mlambda{}z.(c1  z  =\msubz{}  c2  z);J)  =  [])  {}\mRightarrow{}  (\mforall{}j\mmember{}J.((c1  j)  =  0)  \mwedge{}  ((c2  j)  =  1)))


By

---

Latex:
Auto

---

Home Index