---

Step * of Lemma least-closed-set-inductively-defined

∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']
  ∀B:Set{i:l}. ∀G:Set{i:l} ⟶ Set{i:l}.
    ((∀x,a:Set{i:l}.  (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
    ⇒ (∀x,z:Set{i:l}.  ((z ∈ G x) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z])))
    ⇒ inductively-defined{i:l}(x,a.R[x;a];least-closed-set(B;G)))
BY
{ (Auto
   THEN (Assert ∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G a ⊆ G b)) BY
               (Auto
                THEN (RWO "setsubset-iff2" 0 THENA Auto)
                THEN RWO "5" 0
                THEN Auto
                THEN RepeatFor 2 (ParallelLast)
                THEN UseTrans ⌜a⌝⋅
                THEN Auto))
   ) }

1
1. [R] : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
2. B : Set{i:l}
3. G : Set{i:l} ⟶ Set{i:l}
4. ∀x,a:Set{i:l}.  (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b))))
5. ∀x,z:Set{i:l}.  ((z ∈ G x) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z]))
6. ∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G a ⊆ G b))
⊢ inductively-defined{i:l}(x,a.R[x;a];least-closed-set(B;G))

---

Latex:

---

Latex:
\mforall{}[R:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}']
    \mforall{}B:Set\{i:l\}.  \mforall{}G:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}.
        ((\mforall{}x,a:Set\{i:l\}.    (R[x;a]  {}\mRightarrow{}  (\mexists{}b:Set\{i:l\}.  ((b  \mmember{}  B)  \mwedge{}  setimage\{i:l\}(x;b)))))
        {}\mRightarrow{}  (\mforall{}x,z:Set\{i:l\}.    ((z  \mmember{}  G  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}A:Set\{i:l\}.  ((A  \msubseteq{}  x)  \mwedge{}  R[A;z])))
        {}\mRightarrow{}  inductively-defined\{i:l\}(x,a.R[x;a];least-closed-set(B;G)))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}a,b:Set\{i:l\}.    ((a  \msubseteq{}  b)  {}\mRightarrow{}  (G  a  \msubseteq{}  G  b))  BY
                          (Auto
                            THEN  (RWO  "setsubset-iff2"  0  THENA  Auto)
                            THEN  RWO  "5"  0
                            THEN  Auto
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  UseTrans  \mkleeneopen{}a\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  )

---

Home Index