---

Step * 1 1 of Lemma funinv_wf


1. n : ℕ
2. m : ℕ
3. f : ℕn ⟶ ℕm
4. ∀b:ℕm. ∃a:ℕn. ((f a) = b ∈ ℕm)
5. ∀x:ℕm. ((inv(f) x ∈ ℕn) ∧ (↑(f (inv(f) x) =z x)) ∧ (∀[i:ℕn]. ¬↑(f i =z x) supposing i < inv(f) x))
6. inv(f) ∈ ℕm ⟶ ℕn
⊢ Inj(ℕm;ℕn;inv(f))
BY
{ (D 0 THEN Auto THEN (InstHyp [⌜a1⌝] 5⋅ THEN Auto) THEN InstHyp [⌜a2⌝] 5⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m
4.  \mforall{}b:\mBbbN{}m.  \mexists{}a:\mBbbN{}n.  ((f  a)  =  b)
5.  \mforall{}x:\mBbbN{}m
          ((inv(f)  x  \mmember{}  \mBbbN{}n)  \mwedge{}  (\muparrow{}(f  (inv(f)  x)  =\msubz{}  x))  \mwedge{}  (\mforall{}[i:\mBbbN{}n].  \mneg{}\muparrow{}(f  i  =\msubz{}  x)  supposing  i  <  inv(f)  x))
6.  inv(f)  \mmember{}  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n
\mvdash{}  Inj(\mBbbN{}m;\mBbbN{}n;inv(f))


By

---

Latex:
(D  0  THEN  Auto  THEN  (InstHyp  [\mkleeneopen{}a1\mkleeneclose{}]  5\mcdot{}  THEN  Auto)  THEN  InstHyp  [\mkleeneopen{}a2\mkleeneclose{}]  5\mcdot{}  THEN  Auto)

---

Home Index