---

Step * 1 of Lemma nat_add_mon_wf2


∃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
{ Inst [<ℤ+>;λx.x] 0  }

1
.....wf..... 
<ℤ+> ∈ OCMon

2
.....wf..... 
λx.x ∈ |<ℕ,+>| ⟶ |<ℤ+>|

3
IsMonHomInj(<ℕ,+>;<ℤ+>;λx.x)

4
RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x =b y);x,y.↑(x =b y);λx.x)

5
RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);λx.x)

6
.....wf..... 
1. f : |<ℕ,+>| ⟶ |<ℤ+>|
⊢ IsMonHomInj(<ℕ,+>;<ℤ+>;f)
  ∧ RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x =b y);x,y.↑(x =b y);f)
  ∧ RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f) ∈ ℙ

7
.....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)) ∈ ℙ

---

Latex:

---

Latex:

\mexists{}h:OCMon
  \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))


By

---

Latex:
Inst  [<\mBbbZ{}+>\mlambda{}x.x]  0 

---

Home Index