---

Step * of Lemma unsquashed-weak-continuity-base-false

¬base-CP()
BY
{ ((D 0 THENA Auto)
   THEN Unfold `base-CP` -1
   THEN (Skolemize 1 `MC'  THENA (Auto THEN ∀h:hyp. Isect2HD h  THEN Auto))
   THEN Thin 1) }

1
1. MC : F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ
2. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a,b:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕMC F a. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
⊢ False

---

Latex:

---

Latex:
\mneg{}base-CP()


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `base-CP`  -1
  THEN  (Skolemize  1  `MC'    THENA  (Auto  THEN  \mforall{}h:hyp.  Isect2HD  h    THEN  Auto))
  THEN  Thin  1)

---

Home Index