---

Step * of Lemma infinite-domain-example

∀[A,D:Type]. ∀[R,Eq:D ⟶ D ⟶ ℙ].
  ((∀x,y,z:D.  (R[x;y] ⇒ (R[y;z] ∨ Eq[y;z]) ⇒ R[x;z]))
  ⇒ (∀x:D. (R[x;x] ⇒ A))
  ⇒ (∀x:D. ∃y:D. R[x;y])
  ⇒ (∃m:D. ∀x:D. ((Eq[x;m] ⇒ A) ⇒ R[x;m]))
  ⇒ A)
BY
{ ((Auto THEN ExRepD)
   THEN (InstHyp [⌜m⌝] (-3)⋅ THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜y⌝] (-3)⋅ THENA Auto)
   THEN Assert ⌜R[m;m]⌝⋅
   THEN Auto) }

1
.....assertion..... 
1. [A] : Type
2. [D] : Type
3. [R] : D ⟶ D ⟶ ℙ
4. [Eq] : D ⟶ D ⟶ ℙ
5. ∀x,y,z:D.  (R[x;y] ⇒ (R[y;z] ∨ Eq[y;z]) ⇒ R[x;z])@i
6. ∀x:D. (R[x;x] ⇒ A)@i
7. ∀x:D. ∃y:D. R[x;y]@i
8. m : D@i
9. ∀x:D. ((Eq[x;m] ⇒ A) ⇒ R[x;m])@i
10. y : D
11. R[m;y]
12. Eq[y;m]@i
⊢ R[m;m]

2
.....assertion..... 
1. [A] : Type
2. [D] : Type
3. [R] : D ⟶ D ⟶ ℙ
4. [Eq] : D ⟶ D ⟶ ℙ
5. ∀x,y,z:D.  (R[x;y] ⇒ (R[y;z] ∨ Eq[y;z]) ⇒ R[x;z])@i
6. ∀x:D. (R[x;x] ⇒ A)@i
7. ∀x:D. ∃y:D. R[x;y]@i
8. m : D@i
9. ∀x:D. ((Eq[x;m] ⇒ A) ⇒ R[x;m])@i
10. y : D
11. R[m;y]
12. R[y;m]
⊢ R[m;m]

---

Latex:

---

Latex:
\mforall{}[A,D:Type].  \mforall{}[R,Eq:D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y,z:D.    (R[x;y]  {}\mRightarrow{}  (R[y;z]  \mvee{}  Eq[y;z])  {}\mRightarrow{}  R[x;z]))
    {}\mRightarrow{}  (\mforall{}x:D.  (R[x;x]  {}\mRightarrow{}  A))
    {}\mRightarrow{}  (\mforall{}x:D.  \mexists{}y:D.  R[x;y])
    {}\mRightarrow{}  (\mexists{}m:D.  \mforall{}x:D.  ((Eq[x;m]  {}\mRightarrow{}  A)  {}\mRightarrow{}  R[x;m]))
    {}\mRightarrow{}  A)


By

---

Latex:
((Auto  THEN  ExRepD)
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}R[m;m]\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index