---

Step * of Lemma sq_stable__and

∀[P:ℙ]. ∀[Q:⋂p:P. ℙ].  (SqStable(P) ⇒ (P ⇒ SqStable(Q)) ⇒ SqStable(P ∧ Q))
BY
{ (Auto THEN (D 0 THENA (Auto THEN Fold `prop` 0 THEN RenameVar `p' (-1) THEN With ⌜p⌝ (D 2)⋅ THEN Auto))) }

1
1. [P] : ℙ
2. [Q] : ⋂p:P. ℙ
3. SqStable(P)@i
4. P ⇒ SqStable(Q)@i
5. ↓P ∧ Q@i
⊢ P ∧ Q

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  \mforall{}[Q:\mcap{}p:P.  \mBbbP{}].    (SqStable(P)  {}\mRightarrow{}  (P  {}\mRightarrow{}  SqStable(Q))  {}\mRightarrow{}  SqStable(P  \mwedge{}  Q))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  (Auto  THEN  Fold  `prop`  0  THEN  RenameVar  `p'  (-1)  THEN  With  \mkleeneopen{}p\mkleeneclose{}  (D  2)\mcdot{}  THEN  Auto))
  )

---

Home Index