---

Step * 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. (x ∈ f"(a))
⊢ setTC(x) ∈ Set{i:l}
BY
{ (SetMemDef (-1) THEN (InstHyp [⌜b⌝] 3⋅ THENA Auto)) }

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. 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}

---

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.  (x  \mmember{}  f"(a))
\mvdash{}  setTC(x)  \mmember{}  Set\{i:l\}


By

---

Latex:
(SetMemDef  (-1)  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index