---

Step * of Lemma itersetfun-subset-fixpoint

∀G:Set{i:l} ⟶ Set{i:l}
  ((∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G[a] ⊆ G[b])))
  ⇒ (∀X:Set{i:l}. ((G[X] ⊆ X) ⇒ (∀a:Set{i:l}. (itersetfun(x.G[x];a) ⊆ X)))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN SetInduction THEN Auto THEN UseTrans ⌜G[X]⌝⋅ THEN Auto) }

1
.....antecedent..... 
1. G : Set{i:l} ⟶ Set{i:l}
2. ∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G[a] ⊆ G[b]))
3. X : Set{i:l}
4. (G[X] ⊆ X)
5. T : Type
6. f : T ⟶ Set{i:l}
7. ∀t:T. (itersetfun(x.G[x];f[t]) ⊆ X)
⊢ (itersetfun(x.G[x];f"(T)) ⊆ G[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{}X:Set\{i:l\}.  ((G[X]  \msubseteq{}  X)  {}\mRightarrow{}  (\mforall{}a:Set\{i:l\}.  (itersetfun(x.G[x];a)  \msubseteq{}  X)))))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))  THEN  SetInduction  THEN  Auto  THEN  UseTrans  \mkleeneopen{}G[X]\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index