---

Step * 1 1 of Lemma strong-continuity3_functionality_surject


1. T : Type
2. S : Type
3. g : T ⟶ S
4. Surj(T;S;g)
5. F : (ℕ ⟶ S) ⟶ ℕ
6. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F (g o f))) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
8. j : S ⟶ T
9. ∀x:S. ((g (j x)) = x ∈ S)
10. f : ℕ ⟶ S
11. n : ℕ
12. (M n (j o f)) = (inl (F (g o (j o f)))) ∈ (ℕ?)
13. ∀m:ℕ. ((↑isl(M m (j o f))) ⇒ (m = n ∈ ℕ))
⊢ (M n (j o f)) = (inl (F f)) ∈ (ℕ?)
BY
{ (RWO "-2" 0 THEN Auto) }

1
.....subterm..... T:t
1:n
1. T : Type
2. S : Type
3. g : T ⟶ S
4. Surj(T;S;g)
5. F : (ℕ ⟶ S) ⟶ ℕ
6. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F (g o f))) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
8. j : S ⟶ T
9. ∀x:S. ((g (j x)) = x ∈ S)
10. f : ℕ ⟶ S
11. n : ℕ
12. (M n (j o f)) = (inl (F (g o (j o f)))) ∈ (ℕ?)
13. ∀m:ℕ. ((↑isl(M m (j o f))) ⇒ (m = n ∈ ℕ))
⊢ (F (g o (j o f))) = (F f) ∈ ℕ

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  g  :  T  {}\mrightarrow{}  S
4.  Surj(T;S;g)
5.  F  :  (\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}
6.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}?)
7.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}.  (((M  n  f)  =  (inl  (F  (g  o  f))))  \mwedge{}  (\mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  f))  {}\mRightarrow{}  (m  =  n))))
8.  j  :  S  {}\mrightarrow{}  T
9.  \mforall{}x:S.  ((g  (j  x))  =  x)
10.  f  :  \mBbbN{}  {}\mrightarrow{}  S
11.  n  :  \mBbbN{}
12.  (M  n  (j  o  f))  =  (inl  (F  (g  o  (j  o  f))))
13.  \mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  (j  o  f)))  {}\mRightarrow{}  (m  =  n))
\mvdash{}  (M  n  (j  o  f))  =  (inl  (F  f))


By

---

Latex:
(RWO  "-2"  0  THEN  Auto)

---

Home Index