---

Step * of Lemma poset-cat-dist-zero

∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].
  uiff(x = y ∈ cat-ob(poset-cat(I));poset-cat-dist(I;x;y) ≤ 0) supposing cat-arrow(poset-cat(I)) x y
BY
{ (Auto
   THEN InstLemma `extd-nameset-nil` []
   THEN All (RepUR ``cat-ob cat-arrow poset-cat poset-cat-dist name-morph``)
   THEN DVar `x'
   THEN DVar `y'
   THEN Try ((EqTypeCD THEN Auto THEN FunExt THEN Auto))) }

1
1. I : Cname List
2. x : nameset(I) ⟶ extd-nameset([])
3. [%4] : ∀i,j:nameset(I).
            ((↑isname(x i)) ⇒ (↑isname(x j)) ⇒ ((x i) = (x j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(I)))
4. y : nameset(I) ⟶ extd-nameset([])
5. [%6] : ∀i,j:nameset(I).
            ((↑isname(y i)) ⇒ (↑isname(y j)) ⇒ ((y i) = (y j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(I)))
6. ∀x@0:nameset(I). (↑x x@0 ≤z y x@0)
7. x
= y
∈ {f:nameset(I) ⟶ extd-nameset([])| 
   ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(I)))} 
8. extd-nameset([]) ⊆r ℕ2
⊢ ||filter(λi.((x i =z 0) ∧b (y i =z 1));I)|| ≤ 0

2
1. I : Cname List
2. x : nameset(I) ⟶ extd-nameset([])
3. ∀i,j:nameset(I).  ((↑isname(x i)) ⇒ (↑isname(x j)) ⇒ ((x i) = (x j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(I)))
4. y : nameset(I) ⟶ extd-nameset([])
5. ∀i,j:nameset(I).  ((↑isname(y i)) ⇒ (↑isname(y j)) ⇒ ((y i) = (y j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(I)))
6. ∀x@0:nameset(I). (↑x x@0 ≤z y x@0)
7. ||filter(λi.((x i =z 0) ∧b (y i =z 1));I)|| ≤ 0
8. extd-nameset([]) ⊆r ℕ2
9. x1 : nameset(I)
⊢ (x x1) = (y x1) ∈ extd-nameset([])

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y:cat-ob(poset-cat(I))].
    uiff(x  =  y;poset-cat-dist(I;x;y)  \mleq{}  0)  supposing  cat-arrow(poset-cat(I))  x  y


By

---

Latex:
(Auto
  THEN  InstLemma  `extd-nameset-nil`  []
  THEN  All  (RepUR  ``cat-ob  cat-arrow  poset-cat  poset-cat-dist  name-morph``)
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  Try  ((EqTypeCD  THEN  Auto  THEN  FunExt  THEN  Auto)))

---

Home Index