---

Step * 1 of Lemma sigma-unelim-pscm_wf


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. I : cat-ob(C)
6. a1 : X(I)
7. a2 : A(a1)
8. x1 : B(<a1, a2>)
⊢ (a2;x1) ∈ Σ A B(a1)
BY
{ RepeatFor 2 ((RepUR ``presheaf-sigma psc-adjoin-set psc-adjoin`` 0 THEN Auto)) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  I  :  cat-ob(C)
6.  a1  :  X(I)
7.  a2  :  A(a1)
8.  x1  :  B(<a1,  a2>)
\mvdash{}  (a2;x1)  \mmember{}  \mSigma{}  A  B(a1)


By

---

Latex:
RepeatFor  2  ((RepUR  ``presheaf-sigma  psc-adjoin-set  psc-adjoin``  0  THEN  Auto))

---

Home Index