---

Step * 1 1 2 of Lemma itersetfun_functionality_subset


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))
10. x1 : Set{i:l}
11. (x1 ∈ a)
12. (x ∈ itersetfun(x.G[x];x1))
13. b : T
14. seteq(x1;f b)
15. (itersetfun(x.G[x];x1) ⊆ itersetfun(x.G[x];f b))
⊢ (x ∈  ⋃x∈f"(T).itersetfun(x.G[x];x))
BY
{ (Assert (x ∈ itersetfun(x.G[x];f b)) BY
         (RWO "setsubset-iff" (-1) 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))
10. x1 : Set{i:l}
11. (x1 ∈ a)
12. (x ∈ itersetfun(x.G[x];x1))
13. b : T
14. seteq(x1;f b)
15. (itersetfun(x.G[x];x1) ⊆ itersetfun(x.G[x];f b))
16. (x ∈ itersetfun(x.G[x];f b))
⊢ (x ∈  ⋃x∈f"(T).itersetfun(x.G[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.  T  :  Type
4.  f  :  T  {}\mrightarrow{}  Set\{i:l\}
5.  \mforall{}t:T.  \mforall{}a:Set\{i:l\}.    ((a  \msubseteq{}  f[t])  {}\mRightarrow{}  (itersetfun(x.G[x];a)  \msubseteq{}  itersetfun(x.G[x];f[t])))
6.  a  :  Set\{i:l\}
7.  (a  \msubseteq{}  f"(T))
8.  x  :  Set\{i:l\}
9.  (x  \mmember{}    \mcup{}x\mmember{}a.itersetfun(x.G[x];x))
10.  x1  :  Set\{i:l\}
11.  (x1  \mmember{}  a)
12.  (x  \mmember{}  itersetfun(x.G[x];x1))
13.  b  :  T
14.  seteq(x1;f  b)
15.  (itersetfun(x.G[x];x1)  \msubseteq{}  itersetfun(x.G[x];f  b))
\mvdash{}  (x  \mmember{}    \mcup{}x\mmember{}f"(T).itersetfun(x.G[x];x))


By

---

Latex:
(Assert  (x  \mmember{}  itersetfun(x.G[x];f  b))  BY
              (RWO  "setsubset-iff"  (-1)  THEN  Auto))

---

Home Index