---

Step * of Lemma itersetfun_functionality_subset

∀G:Set{i:l} ⟶ Set{i:l}
  ((∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G[a] ⊆ G[b])))
  ⇒ (∀b,a:Set{i:l}.  ((a ⊆ b) ⇒ (itersetfun(x.G[x];a) ⊆ itersetfun(x.G[x];b)))))
BY
{ (RepeatFor 2 (Intro)
   THEN SetInduction
   THEN Auto
   THEN Unfold `itersetfun` 0
   THEN BHyp 2 
   THEN Auto
   THEN RWO "setsubset-iff" 0
   THEN Auto) }

1
1. G : Set{i:l} ⟶ Set{i:l}
2. ∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G[a] ⊆ G[b]))
3. T : Type
4. f : T ⟶ Set{i:l}
5. ∀t:T. ∀a:Set{i:l}.  ((a ⊆ f[t]) ⇒ (itersetfun(x.G[x];a) ⊆ itersetfun(x.G[x];f[t])))
6. a : Set{i:l}
7. (a ⊆ f"(T))
8. x : Set{i:l}
9. (x ∈  ⋃x∈a.itersetfun(x.G[x];x))
⊢ (x ∈  ⋃x∈f"(T).itersetfun(x.G[x];x))

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  SetInduction
  THEN  Auto
  THEN  Unfold  `itersetfun`  0
  THEN  BHyp  2 
  THEN  Auto
  THEN  RWO  "setsubset-iff"  0
  THEN  Auto)

---

Home Index