---

Step * 1 1 1 1 of Lemma transitive-closure-minimal-uniform


1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. Q : A ⟶ A ⟶ ℙ
4. F : x:A ⟶ y:A ⟶ (x R y) ⟶ (x Q y)
5. g : ∀[a,b,c:A].  ((a Q b) ⇒ (b Q c) ⇒ (a Q c))
6. y : A
7. a : A
8. b : A
9. b = y ∈ A
10. q : a Q b
⊢ q ∈ a Q y
BY
{ (HypSubst (-2) (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  Q  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  F  :  x:A  {}\mrightarrow{}  y:A  {}\mrightarrow{}  (x  R  y)  {}\mrightarrow{}  (x  Q  y)
5.  g  :  \mforall{}[a,b,c:A].    ((a  Q  b)  {}\mRightarrow{}  (b  Q  c)  {}\mRightarrow{}  (a  Q  c))
6.  y  :  A
7.  a  :  A
8.  b  :  A
9.  b  =  y
10.  q  :  a  Q  b
\mvdash{}  q  \mmember{}  a  Q  y


By

---

Latex:
(HypSubst  (-2)  (-1)  THEN  Auto)

---

Home Index