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

¬base-CP()
BY
((D THENA Auto)
   THEN Unfold `base-CP` -1
   THEN (Skolemize `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 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