---

Step * 1 of Lemma l_all_exists_max


1. [A] : Type
2. [R] : A ⟶ ℤ ⟶ ℙ
3. ∀x:A. ∀n,m:ℤ.  (R[x;n] ⇒ R[x;m] supposing n ≤ m)@i
⊢ (∀x∈[].∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈[].R[x;n]))
BY
{ (Auto THEN With ⌜0⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [R]  :  A  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:A.  \mforall{}n,m:\mBbbZ{}.    (R[x;n]  {}\mRightarrow{}  R[x;m]  supposing  n  \mleq{}  m)@i
\mvdash{}  (\mforall{}x\mmember{}[].\mexists{}n:\mBbbZ{}.  R[x;n])  {}\mRightarrow{}  (\mexists{}n:\mBbbZ{}.  (\mforall{}x\mmember{}[].R[x;n]))


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index