---

Step * 2 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. (∀x∈v.∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈v.R[x;n]))@i
⊢ (∀x∈[u / v].∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈[u / v].R[x;n]))
BY
{ ((RWO "l_all_cons" 0 THEN Auto) THEN ThinTrivial THEN ExRepD) }

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
⊢ ∃n:ℤ. (R[u;n] ∧ (∀x∈v.R[x;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.  (\mforall{}x\mmember{}v.\mexists{}n:\mBbbZ{}.  R[x;n])  {}\mRightarrow{}  (\mexists{}n:\mBbbZ{}.  (\mforall{}x\mmember{}v.R[x;n]))@i
\mvdash{}  (\mforall{}x\mmember{}[u  /  v].\mexists{}n:\mBbbZ{}.  R[x;n])  {}\mRightarrow{}  (\mexists{}n:\mBbbZ{}.  (\mforall{}x\mmember{}[u  /  v].R[x;n]))


By

---

Latex:
((RWO  "l\_all\_cons"  0  THEN  Auto)  THEN  ThinTrivial  THEN  ExRepD)

---

Home Index