---

Step * of Lemma itersetfun_wf

∀[G:Set{i:l} ⟶ Set{i:l}]. ∀[a:Set{i:l}].  (itersetfun(x.G[x];a) ∈ Set{i:l})
BY
{ (Auto THEN setElim 2) }

1
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}

---

Latex:

---

Latex:
\mforall{}[G:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}].  \mforall{}[a:Set\{i:l\}].    (itersetfun(x.G[x];a)  \mmember{}  Set\{i:l\})


By

---

Latex:
(Auto  THEN  setElim  2)

---

Home Index