---

Step * 1 of Lemma Regularset-regularset


1. A : Set{i:l}
2. transitive-set(A)
3. transitive-set(A)
4. B : coSet{i:l}
5. (B ∈ A)
6. R : coSet{i:l}
7.  setrel(R):(B ⇒ A)
8. ∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
     (SetRelation(R) ⇒  R:(B ⇒ A) ⇒ (∃b:Set{i:l}. ((b ∈ A) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))))
⊢ ∃b:coSet{i:l}. ((b ∈ A) ∧  setrel(R):(B ⇒ b) ∧ setrel(R):(B ─>> b))
BY
{ ((InstHyp [setrel(R)] (-1)⋅ THEN Auto) THEN ParallelLast) }

---

Latex:

---

Latex:

1.  A  :  Set\{i:l\}
2.  transitive-set(A)
3.  transitive-set(A)
4.  B  :  coSet\{i:l\}
5.  (B  \mmember{}  A)
6.  R  :  coSet\{i:l\}
7.    setrel(R):(B  {}\mRightarrow{}  A)
8.  \mforall{}R:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
          (SetRelation(R)  {}\mRightarrow{}    R:(B  {}\mRightarrow{}  A)  {}\mRightarrow{}  (\mexists{}b:Set\{i:l\}.  ((b  \mmember{}  A)  \mwedge{}    R:(B  {}\mRightarrow{}  b)  \mwedge{}  R:(B  {}>>  b))))
\mvdash{}  \mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  A)  \mwedge{}    setrel(R):(B  {}\mRightarrow{}  b)  \mwedge{}  setrel(R):(B  {}>>  b))


By

---

Latex:
((InstHyp  [setrel(R)]  (-1)\mcdot{}  THEN  Auto)  THEN  ParallelLast)

---

Home Index