---

Step * 1 1 1 of Lemma weak-continuity-skolem_functionality


1. T : Type
2. S : Type
3. i : T ⟶ S
4. e1 : Bij(T;S;i)
5. F : (ℕ ⟶ S) ⟶ ℕ
6. M : (ℕ ⟶ T) ⟶ ℕ
7. ∀f,g:ℕ ⟶ T.  ((f = g ∈ (ℕM f ⟶ T)) ⇒ (((λf@0.(F (i o f@0))) f) = ((λf@0.(F (i o f@0))) g) ∈ ℕ))
8. j : S ⟶ T
9. ∀b:S. ((i (j b)) = b ∈ S)
10. ∀a:T. ((j (i a)) = a ∈ T)
11. f : ℕ ⟶ S
12. g : ℕ ⟶ S
13. f = g ∈ (ℕ(λf.(M (j o f))) f ⟶ S)
14. (F (i o (j o f))) = (F (i o (j o g))) ∈ ℕ
⊢ (F f) = (F g) ∈ ℕ
BY
{ (NthHypEq (-1) THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  i  :  T  {}\mrightarrow{}  S
4.  e1  :  Bij(T;S;i)
5.  F  :  (\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}
6.  M  :  (\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  T.    ((f  =  g)  {}\mRightarrow{}  (((\mlambda{}f@0.(F  (i  o  f@0)))  f)  =  ((\mlambda{}f@0.(F  (i  o  f@0)))  g)))
8.  j  :  S  {}\mrightarrow{}  T
9.  \mforall{}b:S.  ((i  (j  b))  =  b)
10.  \mforall{}a:T.  ((j  (i  a))  =  a)
11.  f  :  \mBbbN{}  {}\mrightarrow{}  S
12.  g  :  \mBbbN{}  {}\mrightarrow{}  S
13.  f  =  g
14.  (F  (i  o  (j  o  f)))  =  (F  (i  o  (j  o  g)))
\mvdash{}  (F  f)  =  (F  g)


By

---

Latex:
(NthHypEq  (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index