Step
*
1
1
1
1
1
1
1
1
of Lemma
strong-continuity2-implies-weak-skolem-cantor-nat
1. F : (ā ā¶ š¹) ā¶ ā
2. M : n:ā ā¶ (ān ā¶ š¹) ā¶ (ā?)
3. G : āf:ā ā¶ š¹. ((ān:ā. ((M n f) = (inl (F f)) ā (ā?))) ā§ (ān:ā. (M n f) = (inl (F f)) ā (ā?) supposing āisl(M n f)))
4. f : ā ā¶ š¹
5. g : ā ā¶ š¹
6. n : ā
7. v3 : (M n f) = (inl (F f)) ā (ā?)
8. v2 : ān:ā. (M n f) = (inl (F f)) ā (ā?) supposing āisl(M n f)
9. f = g ā (ān ā¶ š¹)
10. n1 : ā
11. (M n1 g) = (inl (F g)) ā (ā?)
12. ān:ā. (M n g) = (inl (F g)) ā (ā?) supposing āisl(M n g)
13. (M n f) = (M n g) ā (ā?)
14. āisl(M n g)
ā¢ (F f) = (F g) ā ā
BY
{ ((InstHyp [ānā] (-3)ā
THENA Auto) THEN Assert ā(inl (F f)) = (inl (F g)) ā (ā?)āā
THEN Auto) }
Latex:
Latex:
1. F : (\mBbbN{} {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} \mBbbN{}
2. M : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} (\mBbbN{}?)
3. G : \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}
((\mexists{}n:\mBbbN{}. ((M n f) = (inl (F f)))) \mwedge{} (\mforall{}n:\mBbbN{}. (M n f) = (inl (F f)) supposing \muparrow{}isl(M n f)))
4. f : \mBbbN{} {}\mrightarrow{} \mBbbB{}
5. g : \mBbbN{} {}\mrightarrow{} \mBbbB{}
6. n : \mBbbN{}
7. v3 : (M n f) = (inl (F f))
8. v2 : \mforall{}n:\mBbbN{}. (M n f) = (inl (F f)) supposing \muparrow{}isl(M n f)
9. f = g
10. n1 : \mBbbN{}
11. (M n1 g) = (inl (F g))
12. \mforall{}n:\mBbbN{}. (M n g) = (inl (F g)) supposing \muparrow{}isl(M n g)
13. (M n f) = (M n g)
14. \muparrow{}isl(M n g)
\mvdash{} (F f) = (F g)
By
Latex:
((InstHyp [\mkleeneopen{}n\mkleeneclose{}] (-3)\mcdot{} THENA Auto) THEN Assert \mkleeneopen{}(inl (F f)) = (inl (F g))\mkleeneclose{}\mcdot{} THEN Auto)
Home
Index