---

Step * 1 of Lemma representable-psc_wf


1. C : small-category{1:l}
⊢ {G:ps_context{1:l}(C)| ∃I:cat-ob(C). (G = Yoneda(I) ∈ ps_context{1:l}(C))}  ∈ 𝕌{3}
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. C : small-category{1:l}
⊢ ps_context{1:l}(C) ∈ 𝕌{3}

2
.....subterm..... T:t
2:n
1. C : small-category{1:l}
2. G : ps_context{1:l}(C)
⊢ ∃I:cat-ob(C). (G = Yoneda(I) ∈ ps_context{1:l}(C)) ∈ 𝕌{3}

---

Latex:

---

Latex:

1.  C  :  small-category\{1:l\}
\mvdash{}  \{G:ps\_context\{1:l\}(C)|  \mexists{}I:cat-ob(C).  (G  =  Yoneda(I))\}    \mmember{}  \mBbbU{}\{3\}


By

---

Latex:
MemCD

---

Home Index