---

Step * 1 1 2 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. s' : Set{i:l}
11. closed(x,a.R[x;a])s'
12. x : Set{i:l}
13. a : coSet{i:l}
14. (a ∈ r)
15. (x ∈ itersetfun(x.G x;a))
⊢ (x ∈ s')
BY
{ (Assert (itersetfun(x.G x;a) ⊆ s') BY
         (BLemma `itersetfun-subset-fixpoint` 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. s' : Set{i:l}
11. closed(x,a.R[x;a])s'
12. x : Set{i:l}
13. a : coSet{i:l}
14. (a ∈ r)
15. (x ∈ itersetfun(x.G x;a))
⊢ (G s' ⊆ s')

2
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. s' : Set{i:l}
11. closed(x,a.R[x;a])s'
12. x : Set{i:l}
13. a : coSet{i:l}
14. (a ∈ r)
15. (x ∈ itersetfun(x.G x;a))
16. (itersetfun(x.G x;a) ⊆ s')
⊢ (x ∈ s')

---

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.  s'  :  Set\{i:l\}
11.  closed(x,a.R[x;a])s'
12.  x  :  Set\{i:l\}
13.  a  :  coSet\{i:l\}
14.  (a  \mmember{}  r)
15.  (x  \mmember{}  itersetfun(x.G  x;a))
\mvdash{}  (x  \mmember{}  s')


By

---

Latex:
(Assert  (itersetfun(x.G  x;a)  \msubseteq{}  s')  BY
              (BLemma  `itersetfun-subset-fixpoint`  THEN  Auto))

---

Home Index