---

Step * 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))
⊢ inv(f) ∈ {g:ℕm ⟶ ℕn| Inj(ℕm;ℕn;g) ∧ (∀x:ℕm. ((f (g x)) = x ∈ ℤ))} 
BY
{ ((Assert inv(f) ∈ ℕm ⟶ ℕn BY (All (RepUR ``funinv``) THEN MemCD THEN Auto))⋅ THEN MemTypeCD THEN Auto) }

1
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))

2
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 ∈ ℤ

---

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))
\mvdash{}  inv(f)  \mmember{}  \{g:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}m;\mBbbN{}n;g)  \mwedge{}  (\mforall{}x:\mBbbN{}m.  ((f  (g  x))  =  x))\} 


By

---

Latex:
((Assert  inv(f)  \mmember{}  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n  BY
                (All  (RepUR  ``funinv``)  THEN  MemCD  THEN  Auto))\mcdot{}
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index