---

Step * 2 2 1 of Lemma bijection_restriction


1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Inj(ℕk;ℕk;f)
5. ∀b:ℕk. ∃a:ℕk. ((f a) = b ∈ ℕk)
6. (f (k - 1)) = (k - 1) ∈ ℤ
7. f ∈ ℕk - 1 ⟶ ℕk - 1
8. f ∈ ℕk - 1 ⟶ ℕk - 1
9. b : ℕk - 1
10. a : ℕk
11. (f a) = b ∈ ℕk
⊢ ∃a:ℕk - 1. ((f a) = b ∈ ℕk - 1)
BY
{ With ⌜a⌝ (D 0)⋅ }

1
.....wf..... 
1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Inj(ℕk;ℕk;f)
5. ∀b:ℕk. ∃a:ℕk. ((f a) = b ∈ ℕk)
6. (f (k - 1)) = (k - 1) ∈ ℤ
7. f ∈ ℕk - 1 ⟶ ℕk - 1
8. f ∈ ℕk - 1 ⟶ ℕk - 1
9. b : ℕk - 1
10. a : ℕk
11. (f a) = b ∈ ℕk
⊢ a ∈ ℕk - 1

2
1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Inj(ℕk;ℕk;f)
5. ∀b:ℕk. ∃a:ℕk. ((f a) = b ∈ ℕk)
6. (f (k - 1)) = (k - 1) ∈ ℤ
7. f ∈ ℕk - 1 ⟶ ℕk - 1
8. f ∈ ℕk - 1 ⟶ ℕk - 1
9. b : ℕk - 1
10. a : ℕk
11. (f a) = b ∈ ℕk
⊢ (f a) = b ∈ ℕk - 1

3
.....wf..... 
1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Inj(ℕk;ℕk;f)
5. ∀b:ℕk. ∃a:ℕk. ((f a) = b ∈ ℕk)
6. (f (k - 1)) = (k - 1) ∈ ℤ
7. f ∈ ℕk - 1 ⟶ ℕk - 1
8. f ∈ ℕk - 1 ⟶ ℕk - 1
9. b : ℕk - 1
10. a : ℕk
11. (f a) = b ∈ ℕk
12. a1 : ℕk - 1
⊢ (f a1) = b ∈ ℕk - 1 ∈ ℙ

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  f  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}k
3.  0  <  k
4.  Inj(\mBbbN{}k;\mBbbN{}k;f)
5.  \mforall{}b:\mBbbN{}k.  \mexists{}a:\mBbbN{}k.  ((f  a)  =  b)
6.  (f  (k  -  1))  =  (k  -  1)
7.  f  \mmember{}  \mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbN{}k  -  1
8.  f  \mmember{}  \mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbN{}k  -  1
9.  b  :  \mBbbN{}k  -  1
10.  a  :  \mBbbN{}k
11.  (f  a)  =  b
\mvdash{}  \mexists{}a:\mBbbN{}k  -  1.  ((f  a)  =  b)


By

---

Latex:
With  \mkleeneopen{}a\mkleeneclose{}  (D  0)\mcdot{}

---

Home Index