---

Step * 2 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
4. u : A@i
5. v : A List@i
6. n1 : ℤ@i
7. R[u;n1]@i
8. (∀x∈v.∃n:ℤ. R[x;n])@i
9. n : ℤ@i
10. (∀x∈v.R[x;n])@i
⊢ ∃n:ℤ. (R[u;n] ∧ (∀x∈v.R[x;n]))
BY
{ (With ⌜imax(n1;n)⌝ (D 0)⋅ THEN Auto) }

1
1. [A] : Type
2. [R] : A ⟶ ℤ ⟶ ℙ
3. ∀x:A. ∀n,m:ℤ.  (R[x;n] ⇒ R[x;m] supposing n ≤ m)@i
4. u : A@i
5. v : A List@i
6. n1 : ℤ@i
7. R[u;n1]@i
8. (∀x∈v.∃n:ℤ. R[x;n])@i
9. n : ℤ@i
10. (∀x∈v.R[x;n])@i
⊢ R[u;imax(n1;n)]

2
1. [A] : Type
2. [R] : A ⟶ ℤ ⟶ ℙ
3. ∀x:A. ∀n,m:ℤ.  (R[x;n] ⇒ R[x;m] supposing n ≤ m)@i
4. u : A@i
5. v : A List@i
6. n1 : ℤ@i
7. R[u;n1]@i
8. (∀x∈v.∃n:ℤ. R[x;n])@i
9. n : ℤ@i
10. (∀x∈v.R[x;n])@i
11. R[u;imax(n1;n)]
⊢ (∀x∈v.R[x;imax(n1;n)])

---

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
4.  u  :  A@i
5.  v  :  A  List@i
6.  n1  :  \mBbbZ{}@i
7.  R[u;n1]@i
8.  (\mforall{}x\mmember{}v.\mexists{}n:\mBbbZ{}.  R[x;n])@i
9.  n  :  \mBbbZ{}@i
10.  (\mforall{}x\mmember{}v.R[x;n])@i
\mvdash{}  \mexists{}n:\mBbbZ{}.  (R[u;n]  \mwedge{}  (\mforall{}x\mmember{}v.R[x;n]))


By

---

Latex:
(With  \mkleeneopen{}imax(n1;n)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index