---

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

∀I:Cname List. ∀J:nameset(I) List. ∀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
{ (RepeatFor 2 (Intro) THEN Assert ⌜nameset(J) ⊆r nameset(I)⌝⋅) }

1
.....assertion..... 
1. I : Cname List
2. J : nameset(I) List
⊢ nameset(J) ⊆r nameset(I)

2
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)))

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \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:
(RepeatFor  2  (Intro)  THEN  Assert  \mkleeneopen{}nameset(J)  \msubseteq{}r  nameset(I)\mkleeneclose{}\mcdot{})

---

Home Index