---

Step * of Lemma setTC-least

∀a:Set{i:l}. ∀s:coSet{i:l}.  ((a ⊆ s) ⇒ transitive-set(s) ⇒ (setTC(a) ⊆ s))
BY
{ (((RWO "transitive-set-iff" 0 THENA Auto) THEN (RWO "setsubset-iff" 0 THENA Auto)) THEN SetInduction THEN Auto) }

1
1. T : Type
2. f : T ⟶ Set{i:l}
3. ∀t:T. ∀s:coSet{i:l}.
     ((∀x:coSet{i:l}. ((x ∈ f[t]) ⇒ (x ∈ s)))
     ⇒ (∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s)))))
     ⇒ (∀x:coSet{i:l}. ((x ∈ setTC(f[t])) ⇒ (x ∈ s))))
4. s : coSet{i:l}
5. ∀x:coSet{i:l}. ((x ∈ f"(T)) ⇒ (x ∈ s))
6. ∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s))))
7. x : coSet{i:l}
8. (x ∈ setTC(f"(T)))
⊢ (x ∈ s)

---

Latex:

---

Latex:
\mforall{}a:Set\{i:l\}.  \mforall{}s:coSet\{i:l\}.    ((a  \msubseteq{}  s)  {}\mRightarrow{}  transitive-set(s)  {}\mRightarrow{}  (setTC(a)  \msubseteq{}  s))


By

---

Latex:
(((RWO  "transitive-set-iff"  0  THENA  Auto)  THEN  (RWO  "setsubset-iff"  0  THENA  Auto))
  THEN  SetInduction
  THEN  Auto)

---

Home Index