---

Step * 1 of Lemma CCC-Sigma02-dns


1. K : Type
2. CCCNSet(K)
3. P : K ⟶ K ⟶ ℙ
4. ∀k,m:K.  Dec(P[k;m])
5. ∀k:K. (¬(∀m:K. P[k;m]))
6. ∃k:K. ∀m:K. P[k;m]
⊢ False
BY
{ (ExRepD THEN D 5 With ⌜k⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  Type
2.  CCCNSet(K)
3.  P  :  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}k,m:K.    Dec(P[k;m])
5.  \mforall{}k:K.  (\mneg{}(\mforall{}m:K.  P[k;m]))
6.  \mexists{}k:K.  \mforall{}m:K.  P[k;m]
\mvdash{}  False


By

---

Latex:
(ExRepD  THEN  D  5  With  \mkleeneopen{}k\mkleeneclose{}    THEN  Auto)

---

Home Index