---

Step * of Lemma funinv_wf2

∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ].  (inv(f) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )
BY
{ (Auto THEN InstLemma `funinv_wf` [⌜n⌝;⌜n⌝;⌜f⌝]⋅ THEN Auto THEN DoSubsume THEN Auto) }

1
1. n : ℕ
2. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
3. f = f ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⊆r {f:ℕn ⟶ ℕn| Surj(ℕn;ℕn;f)} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  ].    (inv(f)  \mmember{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  )


By

---

Latex:
(Auto  THEN  InstLemma  `funinv\_wf`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  DoSubsume  THEN  Auto)

---

Home Index