---

Step * of Lemma subset-regext

∀a:Set{i:l}. (transitive-set(a) ⇒ (a ⊆ regext(a)))
BY
{ (Auto
   THEN (RWO "setsubset-iff2" 0 THENA Auto)
   THEN SetInduction
   THEN Auto
   THEN setD 1
   THEN (RWO  "setmem-iff" (-1) THENA Auto)
   THEN RepUR ``set-dom set-item mk-set Wsup`` -1
   THEN Fold `Wsup` (-1)
   THEN Fold `mk-set` (-1)
   THEN D -1
   THEN RenameVar `A' 1
   THEN RenameVar `a' 2) }

1
1. A : Type
2. a : A ⟶ Set{i:l}
3. transitive-set(a"(A))
4. T : Type
5. f : T ⟶ Set{i:l}
6. ∀t:T. ((f[t] ∈ a"(A)) ⇒ (f[t] ∈ regext(a"(A))))
7. t : A
8. seteq(f"(T);a t)
⊢ (f"(T) ∈ regext(a"(A)))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RWO  "setsubset-iff2"  0  THENA  Auto)
  THEN  SetInduction
  THEN  Auto
  THEN  setD  1
  THEN  (RWO    "setmem-iff"  (-1)  THENA  Auto)
  THEN  RepUR  ``set-dom  set-item  mk-set  Wsup``  -1
  THEN  Fold  `Wsup`  (-1)
  THEN  Fold  `mk-set`  (-1)
  THEN  D  -1
  THEN  RenameVar  `A'  1
  THEN  RenameVar  `a'  2)

---

Home Index