---

Step * of Lemma pscm-subset-codomain

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

1
.....assertion..... 
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(Y) ∈ psc_map{j:l}(C; Y; Z)
6. x : psc_map{j:l}(C; X; Y)
7. 1(Y) o x ∈ psc_map{j:l}(C; X; Z)
⊢ 1(Y) o x = x ∈ psc_map{j:l}(C; X; Z)

---

Latex:

---

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


By

---

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

---

Home Index