---

Step * 1 of Lemma subset-presheaf-term2


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Y : ps_context{j:l}(C)
4. sub_ps_context{j:l}(C; Y; X)
5. A : {X ⊢ _}
6. {X ⊢ _:A} ⊆r {Y ⊢ _:A}
7. B : {X ⊢ _}
8. A = B ∈ {X ⊢ _}
⊢ {X ⊢ _:A} ⊆r {Y ⊢ _:B}
BY
{ (RWO  "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  Y  :  ps\_context\{j:l\}(C)
4.  sub\_ps\_context\{j:l\}(C;  Y;  X)
5.  A  :  \{X  \mvdash{}  \_\}
6.  \{X  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y  \mvdash{}  \_:A\}
7.  B  :  \{X  \mvdash{}  \_\}
8.  A  =  B
\mvdash{}  \{X  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y  \mvdash{}  \_:B\}


By

---

Latex:
(RWO    "-1"  0  THEN  Auto)

---

Home Index