---

Step * of Lemma setTC_functionality_subset

∀b,a:Set{i:l}.  ((a ⊆ b) ⇒ (setTC(a) ⊆ setTC(b)))
BY
{ (SetInduction THEN Auto) }

1
1. T : Type
2. f : T ⟶ Set{i:l}
3. ∀t:T. ∀a:Set{i:l}.  ((a ⊆ f[t]) ⇒ (setTC(a) ⊆ setTC(f[t])))
4. a : Set{i:l}
5. (a ⊆ f"(T))
⊢ (setTC(a) ⊆ setTC(f"(T)))

---

Latex:

---

Latex:
\mforall{}b,a:Set\{i:l\}.    ((a  \msubseteq{}  b)  {}\mRightarrow{}  (setTC(a)  \msubseteq{}  setTC(b)))


By

---

Latex:
(SetInduction  THEN  Auto)

---

Home Index