---

Step * 1 7 of Lemma nat_add_mon_wf2

.....wf..... 
1. h : OCMon
⊢ ∃f:|<ℕ,+>| ⟶ |h|
   (IsMonHomInj(<ℕ,+>;h;f)
   ∧ RelsIso(|<ℕ,+>|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
   ∧ RelsIso(|<ℕ,+>|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)) ∈ ℙ
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  h  :  OCMon
\mvdash{}  \mexists{}f:|<\mBbbN{},+>|  {}\mrightarrow{}  |h|
      (IsMonHomInj(<\mBbbN{},+>h;f)
      \mwedge{}  RelsIso(|<\mBbbN{},+>|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
      \mwedge{}  RelsIso(|<\mBbbN{},+>|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f))  \mmember{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index