---

Step * 1 2 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
7. Inj(ℕm;ℕn;inv(f))
8. x : ℕm
⊢ (f (inv(f) x)) = x ∈ ℤ
BY
{ (InstHyp [⌜x⌝] (-4)⋅ 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
7.  Inj(\mBbbN{}m;\mBbbN{}n;inv(f))
8.  x  :  \mBbbN{}m
\mvdash{}  (f  (inv(f)  x))  =  x


By

---

Latex:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)

---

Home Index