---

Step * 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)
⊢ (F f) = (F g) ∈ ℕ
BY
{ ((InstHyp [⌜j o f⌝;⌜j o g⌝] (-7)⋅ THENA Auto) THEN Reduce -1) }

1
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) ∈ ℕ

---

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
\mvdash{}  (F  f)  =  (F  g)


By

---

Latex:
((InstHyp  [\mkleeneopen{}j  o  f\mkleeneclose{};\mkleeneopen{}j  o  g\mkleeneclose{}]  (-7)\mcdot{}  THENA  Auto)  THEN  Reduce  -1)

---

Home Index