---

Step * of Lemma ppcc-test3

∀[T:Type]
  ∀f:T ⟶ T
    ∀[Q,P:T ⟶ T ⟶ ℙ].
      ((∀a,b:T.  (Q[f[a];b] ⇐⇒ P[a;f[b]]))
      ⇒ Trans(T;a,b.P[a;b])
      ⇒ (∀a,b,c,d,e,x:T.  (P[a;c] ⇒ Q[d;b] ⇒ P[a;e]) supposing ((f[b] = e ∈ T) and (f[x] = d ∈ T) and (c = x ∈ T))))
BY
{ (UnivCD THENA Auto) }

1
1. [T] : Type
2. f : T ⟶ T
3. [Q] : T ⟶ T ⟶ ℙ
4. [P] : T ⟶ T ⟶ ℙ
5. ∀a,b:T.  (Q[f[a];b] ⇐⇒ P[a;f[b]])
6. Trans(T;a,b.P[a;b])
7. a : T
8. b : T
9. c : T
10. d : T
11. e : T
12. x : T
13. c = x ∈ T
14. f[x] = d ∈ T
15. f[b] = e ∈ T
16. P[a;c]
17. Q[d;b]
⊢ P[a;e]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  T
        \mforall{}[Q,P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
            ((\mforall{}a,b:T.    (Q[f[a];b]  \mLeftarrow{}{}\mRightarrow{}  P[a;f[b]]))
            {}\mRightarrow{}  Trans(T;a,b.P[a;b])
            {}\mRightarrow{}  (\mforall{}a,b,c,d,e,x:T.
                        (P[a;c]  {}\mRightarrow{}  Q[d;b]  {}\mRightarrow{}  P[a;e])  supposing  ((f[b]  =  e)  and  (f[x]  =  d)  and  (c  =  x))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index