---

Step * 1 1 1 of Lemma setTC_wf


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}
BY
{ ((Subst' Wsup(a;f) ~ f"(a) 0 THENA Computation) THEN (MemCD THENA Auto) THEN D -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})
4. x : Set{i:l}
5. (x ∈ f"(a))
⊢ setTC(x) ∈ Set{i:l}

---

Latex:

---

Latex:

1.  a  :  Type
2.  f  :  a  {}\mrightarrow{}  Set\{i:l\}
3.  \mforall{}b:a.  (\mlambda{}x.setTC(x)  \mmember{}  \{x:Set\{i:l\}|  (x  \mmember{}  f  b)\}    {}\mrightarrow{}  Set\{i:l\})
\mvdash{}  \mlambda{}x.setTC(x)  \mmember{}  \{x@0:Set\{i:l\}|  (x@0  \mmember{}  Wsup(a;f))\}    {}\mrightarrow{}  Set\{i:l\}


By

---

Latex:
((Subst'  Wsup(a;f)  \msim{}  f"(a)  0  THENA  Computation)  THEN  (MemCD  THENA  Auto)  THEN  D  -1)

---

Home Index