---

Step * of Lemma subset-presheaf-term

No Annotations
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].
  ∀[A:{X ⊢ _}]. ({X ⊢ _:A} ⊆r {Y ⊢ _:A}) supposing sub_ps_context{j:l}(C; Y; X)
BY
{ (InstLemma `subset-presheaf-type` []
   THEN RepeatFor 4 (ParallelLast')
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN DupHyp 4
   THEN Unfold `sub_ps_context` -1
   THEN (Assert (x)1(Y) ∈ {Y ⊢ _:(A)1(Y)} BY
               Auto)
   THEN (Enough to prove (x)1(Y) = x ∈ {Y ⊢ _:A}
          Because Eq)) }

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. {X ⊢ _} ⊆r {Y ⊢ _}
6. A : {X ⊢ _}
7. x : {X ⊢ _:A}
8. 1(Y) ∈ psc_map{j:l}(C; Y; X)
9. (x)1(Y) ∈ {Y ⊢ _:(A)1(Y)}
⊢ (x)1(Y) = x ∈ {Y ⊢ _:A}

---

Latex:

---

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


By

---

Latex:
(InstLemma  `subset-presheaf-type`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  DupHyp  4
  THEN  Unfold  `sub\_ps\_context`  -1
  THEN  (Assert  (x)1(Y)  \mmember{}  \{Y  \mvdash{}  \_:(A)1(Y)\}  BY
                          Auto)
  THEN  (Enough  to  prove  (x)1(Y)  =  x
                Because  Eq))

---

Home Index