---

Step * of Lemma pscm-subset-domain

No Annotations
∀[C:SmallCategory]. ∀[X,Y,Z:ps_context{j:l}(C)].
  psc_map{j:l}(C; Y; X) ⊆r psc_map{j:l}(C; Z; X) supposing sub_ps_context{j:l}(C; Z; Y)
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN Unfold `sub_ps_context` -2
   THEN (InstLemma `pscm-comp_wf` [⌜C⌝;⌜Z⌝;⌜Y⌝;⌜X⌝;⌜1(Z)⌝;⌜x⌝]⋅ THENA Auto)
   THEN Assert ⌜x o 1(Z) = x ∈ psc_map{j:l}(C; Z; X)⌝⋅
   THEN Try (Eq)
   THEN (EqTypeCD THENW Auto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Y : ps_context{j:l}(C)
4. Z : ps_context{j:l}(C)
5. 1(Z) ∈ psc_map{j:l}(C; Z; Y)
6. x : psc_map{j:l}(C; Y; X)
7. x o 1(Z) ∈ psc_map{j:l}(C; Z; X)
⊢ x o 1(Z) = x ∈ (A:cat-ob(op-cat(C)) ⟶ (cat-arrow(type-cat{j':l}) (Z A) (X A)))

2
.....set predicate..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Y : ps_context{j:l}(C)
4. Z : ps_context{j:l}(C)
5. 1(Z) ∈ psc_map{j:l}(C; Z; Y)
6. x : psc_map{j:l}(C; Y; X)
7. x o 1(Z) ∈ psc_map{j:l}(C; Z; X)
⊢ ∀A,B:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A B.
    ((cat-comp(type-cat{j':l}) (Z A) (X A) (X B) (x o 1(Z) A) (X A B g))
    = (cat-comp(type-cat{j':l}) (Z A) (Z B) (X B) (Z A B g) (x o 1(Z) B))
    ∈ (cat-arrow(type-cat{j':l}) (Z A) (X B)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X,Y,Z:ps\_context\{j:l\}(C)].
    psc\_map\{j:l\}(C;  Y;  X)  \msubseteq{}r  psc\_map\{j:l\}(C;  Z;  X)  supposing  sub\_ps\_context\{j:l\}(C;  Z;  Y)


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `sub\_ps\_context`  -2
  THEN  (InstLemma  `pscm-comp\_wf`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}1(Z)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}x  o  1(Z)  =  x\mkleeneclose{}\mcdot{}
  THEN  Try  (Eq)
  THEN  (EqTypeCD  THENW  Auto))

---

Home Index