---

Step * 1 of Lemma itersetfun_wf


1. G : Set{i:l} ⟶ Set{i:l}
2. a1 : Type
3. f : a1 ⟶ Set{i:l}
4. ∀b:a1. (itersetfun(x.G[x];f b) ∈ Set{i:l})
⊢ itersetfun(x.G[x];Wsup(a1;f)) ∈ Set{i:l}
BY
{ (Unfold `itersetfun` 0 THEN MemCD THEN Try (Trivial) THEN Unfold `setunionfun` 0 THEN RepUR ``Wsup`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}
2.  a1  :  Type
3.  f  :  a1  {}\mrightarrow{}  Set\{i:l\}
4.  \mforall{}b:a1.  (itersetfun(x.G[x];f  b)  \mmember{}  Set\{i:l\})
\mvdash{}  itersetfun(x.G[x];Wsup(a1;f))  \mmember{}  Set\{i:l\}


By

---

Latex:
(Unfold  `itersetfun`  0
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  Unfold  `setunionfun`  0
  THEN  RepUR  ``Wsup``  0
  THEN  Auto)

---

Home Index