---

Step * of Lemma setTC-transitive

∀a:Set{i:l}. transitive-set(setTC(a))
BY
{ (((RWO "transitive-set-iff" 0 THENA Auto) THEN (RWO "setsubset-iff" 0 THENA Auto))
   THEN (SetInduction THENA Auto)
   THEN RepeatFor 3 ((D 0 THENA Auto))) }

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

---

Latex:

---

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


By

---

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

---

Home Index