---

Step * 2 of Lemma uimplies-iff-squash-implies


1. [P] : ℙ
2. [Q] : ℙ
3. Image(P,(λx.Ax)) ⇒ Q@i
4. [%1] : P
⊢ Q
BY
{ (D (-2) THEN Auto) }

1
.....antecedent..... 
1. [P] : ℙ
2. [Q] : ℙ
3. [%1] : P
⊢ Image(P,(λx.Ax))

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  Image(P,(\mlambda{}x.Ax))  {}\mRightarrow{}  Q@i
4.  [\%1]  :  P
\mvdash{}  Q


By

---

Latex:
(D  (-2)  THEN  Auto)

---

Home Index