---

Step * 1 1 of Lemma setTC-least


1. T : Type
2. f : T ⟶ Set{i:l}
3. ∀t:T. ∀s:coSet{i:l}.
     ((∀x:coSet{i:l}. ((x ∈ f[t]) ⇒ (x ∈ s)))
     ⇒ (∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s)))))
     ⇒ (∀x:coSet{i:l}. ((x ∈ setTC(f[t])) ⇒ (x ∈ s))))
4. s : coSet{i:l}
5. ∀x:coSet{i:l}. ((x ∈ f"(T)) ⇒ (x ∈ s))
6. ∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s))))
7. x : coSet{i:l}
8. x1 : coSet{i:l}
9. (x1 ∈ f"(T))
10. (x ∈ setTC(x1))
⊢ (x ∈ s)
BY
{ ((Assert (x1 ∈ s) BY Auto) THEN SetMemDef (-3) THEN ExRepD THEN InstHyp [⌜b⌝;⌜s⌝;⌜x⌝] 3⋅ THEN Auto) }

1
1. T : Type
2. f : T ⟶ Set{i:l}
3. ∀t:T. ∀s:coSet{i:l}.
     ((∀x:coSet{i:l}. ((x ∈ f[t]) ⇒ (x ∈ s)))
     ⇒ (∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s)))))
     ⇒ (∀x:coSet{i:l}. ((x ∈ setTC(f[t])) ⇒ (x ∈ s))))
4. s : coSet{i:l}
5. ∀x:coSet{i:l}. ((x ∈ f"(T)) ⇒ (x ∈ s))
6. ∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s))))
7. x : coSet{i:l}
8. x1 : coSet{i:l}
9. b : T
10. seteq(x1;f b)
11. (x ∈ setTC(x1))
12. (x1 ∈ s)
13. x2 : coSet{i:l}
14. (x2 ∈ f[b])
⊢ (x2 ∈ s)

2
.....antecedent..... 
1. T : Type
2. f : T ⟶ Set{i:l}
3. ∀t:T. ∀s:coSet{i:l}.
     ((∀x:coSet{i:l}. ((x ∈ f[t]) ⇒ (x ∈ s)))
     ⇒ (∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s)))))
     ⇒ (∀x:coSet{i:l}. ((x ∈ setTC(f[t])) ⇒ (x ∈ s))))
4. s : coSet{i:l}
5. ∀x:coSet{i:l}. ((x ∈ f"(T)) ⇒ (x ∈ s))
6. ∀x:coSet{i:l}. ((x ∈ s) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ s))))
7. x : coSet{i:l}
8. x1 : coSet{i:l}
9. b : T
10. seteq(x1;f b)
11. (x ∈ setTC(x1))
12. (x1 ∈ s)
⊢ (x ∈ setTC(f[b]))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  Set\{i:l\}
3.  \mforall{}t:T.  \mforall{}s:coSet\{i:l\}.
          ((\mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  f[t])  {}\mRightarrow{}  (x  \mmember{}  s)))
          {}\mRightarrow{}  (\mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  s)  {}\mRightarrow{}  (\mforall{}x1:coSet\{i:l\}.  ((x1  \mmember{}  x)  {}\mRightarrow{}  (x1  \mmember{}  s)))))
          {}\mRightarrow{}  (\mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  setTC(f[t]))  {}\mRightarrow{}  (x  \mmember{}  s))))
4.  s  :  coSet\{i:l\}
5.  \mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  f"(T))  {}\mRightarrow{}  (x  \mmember{}  s))
6.  \mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  s)  {}\mRightarrow{}  (\mforall{}x1:coSet\{i:l\}.  ((x1  \mmember{}  x)  {}\mRightarrow{}  (x1  \mmember{}  s))))
7.  x  :  coSet\{i:l\}
8.  x1  :  coSet\{i:l\}
9.  (x1  \mmember{}  f"(T))
10.  (x  \mmember{}  setTC(x1))
\mvdash{}  (x  \mmember{}  s)


By

---

Latex:
((Assert  (x1  \mmember{}  s)  BY  Auto)  THEN  SetMemDef  (-3)  THEN  ExRepD  THEN  InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THEN  Auto)

---

Home Index