---

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


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))
7. r : Set{i:l}
8. Regular(r)
9. (B ⊆ r)
10. Y : Set{i:l}
11. y : Set{i:l}
12. (Y ⊆  ⋃a∈r.itersetfun(x.G x;a))
13. R[Y;y]
14. b : Set{i:l}
15. setimage{i:l}(Y;b)
16. (b ∈ r)
⊢ (y ∈  ⋃a∈r.itersetfun(x.G x;a))
BY
{ (RenameVar `a' (-3)
   THEN D -2
   THEN (Assert ∀x:Set{i:l}. ∀m:(x ∈ a).  (f <x, m> ∈  ⋃a∈r.itersetfun(x.G x;a)) BY
               (Auto
                THEN (InstHyp [⌜f <x, m>⌝] (-4)⋅ THENA Auto)
                THEN (RepeatFor 2 (D -1) THENA (D 0 With ⌜<x, m>⌝  THEN Auto))
                THEN RWO "setsubset-iff" (-11)
                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))
7. r : Set{i:l}
8. Regular(r)
9. (B ⊆ r)
10. Y : Set{i:l}
11. y : Set{i:l}
12. (Y ⊆  ⋃a∈r.itersetfun(x.G x;a))
13. R[Y;y]
14. a : Set{i:l}
15. f : (z:coSet{i:l} × (z ∈ a)) ⟶ coSet{i:l}
16. (∀z1,z2:z:coSet{i:l} × (z ∈ a).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2)))
∧ (∀y:coSet{i:l}. ((y ∈ Y) ⇐⇒ ∃z:z:coSet{i:l} × (z ∈ a). seteq(y;f z)))
17. (a ∈ r)
18. ∀x:Set{i:l}. ∀m:(x ∈ a).  (f <x, m> ∈  ⋃a∈r.itersetfun(x.G x;a))
⊢ (y ∈  ⋃a∈r.itersetfun(x.G x;a))

---

Latex:

---

Latex:

1.  [R]  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
2.  B  :  Set\{i:l\}
3.  G  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}
4.  \mforall{}x,a:Set\{i:l\}.    (R[x;a]  {}\mRightarrow{}  (\mexists{}b:Set\{i:l\}.  ((b  \mmember{}  B)  \mwedge{}  setimage\{i:l\}(x;b))))
5.  \mforall{}x,z:Set\{i:l\}.    ((z  \mmember{}  G  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}A:Set\{i:l\}.  ((A  \msubseteq{}  x)  \mwedge{}  R[A;z]))
6.  \mforall{}a,b:Set\{i:l\}.    ((a  \msubseteq{}  b)  {}\mRightarrow{}  (G  a  \msubseteq{}  G  b))
7.  r  :  Set\{i:l\}
8.  Regular(r)
9.  (B  \msubseteq{}  r)
10.  Y  :  Set\{i:l\}
11.  y  :  Set\{i:l\}
12.  (Y  \msubseteq{}    \mcup{}a\mmember{}r.itersetfun(x.G  x;a))
13.  R[Y;y]
14.  b  :  Set\{i:l\}
15.  setimage\{i:l\}(Y;b)
16.  (b  \mmember{}  r)
\mvdash{}  (y  \mmember{}    \mcup{}a\mmember{}r.itersetfun(x.G  x;a))


By

---

Latex:
(RenameVar  `a'  (-3)
  THEN  D  -2
  THEN  (Assert  \mforall{}x:Set\{i:l\}.  \mforall{}m:(x  \mmember{}  a).    (f  <x,  m>  \mmember{}    \mcup{}a\mmember{}r.itersetfun(x.G  x;a))  BY
                          (Auto
                            THEN  (InstHyp  [\mkleeneopen{}f  <x,  m>\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
                            THEN  (RepeatFor  2  (D  -1)  THENA  (D  0  With  \mkleeneopen{}<x,  m>\mkleeneclose{}    THEN  Auto))
                            THEN  RWO  "setsubset-iff"  (-11)
                            THEN  Auto)))

---

Home Index