---

Step * 1 2 1 of Lemma setTC_wf


1. a : Set{i:l}
2. ∀s:Set{i:l}. (λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ s)}  ⟶ Set{i:l})
3. λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ (a)+)}  ⟶ Set{i:l}
⊢ setTC(a) ∈ Set{i:l}
BY
{ ((Subst' setTC(a) ~ (λx.setTC(x)) a 0 THENA (Reduce 0 THEN Auto)) THEN MemCD) }

1
.....subterm..... T:t
1:n
1. a : Set{i:l}
2. ∀s:Set{i:l}. (λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ s)}  ⟶ Set{i:l})
3. λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ (a)+)}  ⟶ Set{i:l}
⊢ λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ (a)+)}  ⟶ Set{i:l}

2
.....subterm..... T:t
2:n
1. a : Set{i:l}
2. ∀s:Set{i:l}. (λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ s)}  ⟶ Set{i:l})
3. λx.setTC(x) ∈ {x:Set{i:l}| (x ∈ (a)+)}  ⟶ Set{i:l}
⊢ a ∈ {x:Set{i:l}| (x ∈ (a)+)} 

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  setTC(a)  \msim{}  (\mlambda{}x.setTC(x))  a  0  THENA  (Reduce  0  THEN  Auto))  THEN  MemCD)

---

Home Index