---

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


1. P : ℙ
2. Q : ℙ
3. P
⊢ Ax ∈ Image(P,(λx.Ax))
BY
{ Assert ⌜(λx.Ax) %1 ∈ Image(P,(λx.Ax))⌝⋅ }

1
.....assertion..... 
1. P : ℙ
2. Q : ℙ
3. P
⊢ (λx.Ax) %1 ∈ Image(P,(λx.Ax))

2
1. P : ℙ
2. Q : ℙ
3. P
4. (λx.Ax) %1 ∈ Image(P,(λx.Ax))
⊢ Ax ∈ Image(P,(λx.Ax))

---

Latex:

---

Latex:

1.  P  :  \mBbbP{}
2.  Q  :  \mBbbP{}
3.  P
\mvdash{}  Ax  \mmember{}  Image(P,(\mlambda{}x.Ax))


By

---

Latex:
Assert  \mkleeneopen{}(\mlambda{}x.Ax)  \%1  \mmember{}  Image(P,(\mlambda{}x.Ax))\mkleeneclose{}\mcdot{}

---

Home Index