---

Step * of Lemma flip_bijection

∀k:ℕ. ∀i,j:ℕk.  Bij(ℕk;ℕk;(i, j))
BY
{ ((Unfold `biject` 0 THEN Unfolds ``inject surject`` 0) THEN Auto) }

1
1. k : ℕ
2. i : ℕk
3. j : ℕk
4. a1 : ℕk
5. a2 : ℕk
6. ((i, j) a1) = ((i, j) a2) ∈ ℕk
⊢ a1 = a2 ∈ ℕk

2
1. k : ℕ
2. i : ℕk
3. j : ℕk
4. ∀a1,a2:ℕk.  ((((i, j) a1) = ((i, j) a2) ∈ ℕk) ⇒ (a1 = a2 ∈ ℕk))
5. b : ℕk
⊢ ∃a:ℕk. (((i, j) a) = b ∈ ℕk)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}i,j:\mBbbN{}k.    Bij(\mBbbN{}k;\mBbbN{}k;(i,  j))


By

---

Latex:
((Unfold  `biject`  0  THEN  Unfolds  ``inject  surject``  0)  THEN  Auto)

---

Home Index