---

Step * 2 of Lemma flip_bijection


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)
BY
{ (InstConcl [(i, j) b] THENA Auto) }

1
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
⊢ ((i, j) ((i, j) b)) = b ∈ ℕk

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  i  :  \mBbbN{}k
3.  j  :  \mBbbN{}k
4.  \mforall{}a1,a2:\mBbbN{}k.    ((((i,  j)  a1)  =  ((i,  j)  a2))  {}\mRightarrow{}  (a1  =  a2))
5.  b  :  \mBbbN{}k
\mvdash{}  \mexists{}a:\mBbbN{}k.  (((i,  j)  a)  =  b)


By

---

Latex:
(InstConcl  [(i,  j)  b]  THENA  Auto)

---

Home Index