---

Step * 1 1 of Lemma setTC_wf

.....assertion..... 
1. a : Set{i:l}
⊢ ∀s:Set{i:l}. (λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ s)}  ⟶ Set{i:l})
BY
{ (Thin (-1) THEN Intro THEN setElim 1) }

1
1. a : Type
2. f : a ⟶ Set{i:l}
3. ∀b:a. (λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ f b)}  ⟶ Set{i:l})
⊢ λx.setTC(x) ∈ {x@0:Set{i:l}| (x@0 ∈ Wsup(a;f))}  ⟶ Set{i:l}

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  Set\{i:l\}
\mvdash{}  \mforall{}s:Set\{i:l\}.  (\mlambda{}x.setTC(x)  \mmember{}  \{x:Set\{i:l\}|  (x  \mmember{}  s)\}    {}\mrightarrow{}  Set\{i:l\})


By

---

Latex:
(Thin  (-1)  THEN  Intro  THEN  setElim  1)

---

Home Index