---

Step * of Lemma subset-presheaf-term2

No Annotations
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].
  ∀[A,B:{X ⊢ _}].  {X ⊢ _:A} ⊆r {Y ⊢ _:B} supposing A = B ∈ {X ⊢ _} supposing sub_ps_context{j:l}(C; Y; X)
BY
{ (InstLemma `subset-presheaf-term` [] THEN RepeatFor 5 (ParallelLast') THEN Auto) }

1
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}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X,Y:ps\_context\{j:l\}(C)].
    \mforall{}[A,B:\{X  \mvdash{}  \_\}].    \{X  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y  \mvdash{}  \_:B\}  supposing  A  =  B  supposing  sub\_ps\_context\{j:l\}(C;  Y;  X)


By

---

Latex:
(InstLemma  `subset-presheaf-term`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  Auto)

---

Home Index