---

Step * 1 of Lemma ancestral-logic-example1


⊢ (∀x,y:Dom.  ((P x y) ⇒ (Q x y))) ⇒ (∀x,y:Dom.  (TC(λa,b.P a b)(x,y) ⇒ TC(λa,b.Q a b)(x,y)))
BY
{ (FOImpliesIntro THEN Assert ⌈∀x,y:Dom.  ((P x y) ⇒ TC(λa,b.Q a b)(x,y))⌉⋅) }

1
.....assertion..... 
9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
⊢ ∀x,y:Dom.  ((P x y) ⇒ TC(λa,b.Q a b)(x,y))

2
9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
10. ∀x,y:Dom.  ((P x y) ⇒ TC(λa,b.Q a b)(x,y))
⊢ ∀x,y:Dom.  (TC(λa,b.P a b)(x,y) ⇒ TC(λa,b.Q a b)(x,y))

---

Latex:



\mvdash{}  (\mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  (Q  x  y)))  {}\mRightarrow{}  (\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.P  a  b)(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.Q  a  b)(x,y)))


By

(FOImpliesIntro  THEN  Assert  \mkleeneopen{}\mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  TC(\mlambda{}a,b.Q  a  b)(x,y))\mkleeneclose{}\mcdot{})

---

Home Index