Step
*
1
1
1
1
1
1
1
of Lemma
strong-continuity2-implies-weak-skolem-cantor
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)
⊢ F f = F g
BY
{ xxx((Assert ⌜(M n f) = (M n g) ∈ (𝔹?)⌝⋅ THENA Auto) THEN (Assert ⌜↑isl(M n g)⌝⋅ THENA Auto))xxx }
1
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
Latex:
Latex:
1. F : (\mBbbN{} {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} \mBbbB{}
2. M : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} (\mBbbB{}?)
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)
\mvdash{} F f = F g
By
Latex:
xxx((Assert \mkleeneopen{}(M n f) = (M n g)\mkleeneclose{}\mcdot{} THENA Auto) THEN (Assert \mkleeneopen{}\muparrow{}isl(M n g)\mkleeneclose{}\mcdot{} THENA Auto))xxx
Home
Index