---

Step * 1 1 1 1 of Lemma itersetfun-subset-fixpoint


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)
8. x : Set{i:l}
9. x1 : coSet{i:l}
10. b : T
11. seteq(x1;f b)
12. (x ∈ itersetfun(x.G[x];x1))
⊢ (x ∈ X)
BY
{ (FLemma `coSet-seteq-Set` [-2] THENA Auto) }

1
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)
8. x : Set{i:l}
9. x1 : coSet{i:l}
10. b : T
11. seteq(x1;f b)
12. (x ∈ itersetfun(x.G[x];x1))
13. x1 ∈ Set{i:l}
⊢ (x ∈ X)

---

Latex:

---

Latex:

1.  G  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}
2.  \mforall{}a,b:Set\{i:l\}.    ((a  \msubseteq{}  b)  {}\mRightarrow{}  (G[a]  \msubseteq{}  G[b]))
3.  X  :  Set\{i:l\}
4.  (G[X]  \msubseteq{}  X)
5.  T  :  Type
6.  f  :  T  {}\mrightarrow{}  Set\{i:l\}
7.  \mforall{}t:T.  (itersetfun(x.G[x];f[t])  \msubseteq{}  X)
8.  x  :  Set\{i:l\}
9.  x1  :  coSet\{i:l\}
10.  b  :  T
11.  seteq(x1;f  b)
12.  (x  \mmember{}  itersetfun(x.G[x];x1))
\mvdash{}  (x  \mmember{}  X)


By

---

Latex:
(FLemma  `coSet-seteq-Set`  [-2]  THENA  Auto)

---

Home Index