---

Step * 1 1 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})
4. x : Set{i:l}
5. b : a
6. seteq(x;f b)
7. λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ f b)}  ⟶ Set{i:l}
⊢ setTC(x) ∈ Set{i:l}
BY
{ (Unfold `setTC` 0 THEN Auto THEN (Subst' setTC(x1) ~ (λx.setTC(x)) x1 0 THENA (Reduce 0 THEN Auto)) THEN Auto) }

---

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\})
4.  x  :  Set\{i:l\}
5.  b  :  a
6.  seteq(x;f  b)
7.  \mlambda{}x.setTC(x)  \mmember{}  \{x:Set\{i:l\}|  (x  \mmember{}  f  b)\}    {}\mrightarrow{}  Set\{i:l\}
\mvdash{}  setTC(x)  \mmember{}  Set\{i:l\}


By

---

Latex:
(Unfold  `setTC`  0
  THEN  Auto
  THEN  (Subst'  setTC(x1)  \msim{}  (\mlambda{}x.setTC(x))  x1  0  THENA  (Reduce  0  THEN  Auto))
  THEN  Auto)

---

Home Index