---

Step * of Lemma uimplies-iff-squash-implies

∀[P,Q:ℙ].  (Q supposing P ⇐⇒ (↓P) ⇒ Q)
BY
{ (RepUR ``uimplies squash`` 0 THEN Auto) }

1
1. [P] : ℙ
2. [Q] : ℙ
3. ⋂:P. Q@i
4. Image(P,(λx.Ax))@i
⊢ Q

2
1. [P] : ℙ
2. [Q] : ℙ
3. Image(P,(λx.Ax)) ⇒ Q@i
4. [%1] : P
⊢ Q

---

Latex:

---

Latex:
\mforall{}[P,Q:\mBbbP{}].    (Q  supposing  P  \mLeftarrow{}{}\mRightarrow{}  (\mdownarrow{}P)  {}\mRightarrow{}  Q)


By

---

Latex:
(RepUR  ``uimplies  squash``  0  THEN  Auto)

---

Home Index