---

Step * of Lemma setmem-sub-set

∀s:Set{i:l}
  ∀[P:{a:Set{i:l}| (a ∈ s)}  ⟶ ℙ]
    (set-predicate{i:l}(s;a.P[a]) ⇒ (∀a:Set{i:l}. ((a ∈ {a ∈ s | P[a]}) ⇐⇒ (a ∈ s) ∧ P[a])))
BY
{ (Auto
   THEN setD 1
   THEN All (\h. ((RepUR ``sub-set`` h THEN Fold `Wsup` h THEN Fold `mk-set` h)
                  THEN (RWO "setmem-mk-set-sq" h THENA Auto)
                  THEN Reduce h) )⋅
   THEN ExRepD
   THEN Try (DProds)
   THEN All Reduce
   THEN Auto) }

1
1. T : Type
2. f : T ⟶ Set{i:l}
3. [P] : {a:Set{i:l}| (a ∈ f"(T))}  ⟶ ℙ
4. set-predicate{i:l}(f"(T);a.P[a])
5. a : Set{i:l}
6. t : T
7. b1 : P[f t]
8. seteq(a;f t)
⊢ P[a]

2
1. T : Type
2. f : T ⟶ Set{i:l}
3. [P] : {a:Set{i:l}| (a ∈ f"(T))}  ⟶ ℙ
4. set-predicate{i:l}(f"(T);a.P[a])
5. a : Set{i:l}
6. (a ∈ f"(T))
7. P[a]
⊢ ∃b:t:T × P[f t]. seteq(a;f (fst(b)))

---

Latex:

---

Latex:
\mforall{}s:Set\{i:l\}
    \mforall{}[P:\{a:Set\{i:l\}|  (a  \mmember{}  s)\}    {}\mrightarrow{}  \mBbbP{}]
        (set-predicate\{i:l\}(s;a.P[a])  {}\mRightarrow{}  (\mforall{}a:Set\{i:l\}.  ((a  \mmember{}  \{a  \mmember{}  s  |  P[a]\})  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  s)  \mwedge{}  P[a])))


By

---

Latex:
(Auto
  THEN  setD  1
  THEN  All  (\mbackslash{}h.  ((RepUR  ``sub-set``  h  THEN  Fold  `Wsup`  h  THEN  Fold  `mk-set`  h)
                                THEN  (RWO  "setmem-mk-set-sq"  h  THENA  Auto)
                                THEN  Reduce  h)  )\mcdot{}
  THEN  ExRepD
  THEN  Try  (DProds)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index