---

Step * of Lemma finite-set-type

∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. SqStable(P[x])) ⇒ (finite-type({x:T| P[x]} ) ⇐⇒ ∃L:T List. ∀x:T. (P[x] ⇐⇒ (x ∈ L))))
BY
{ TACTIC:(RepeatFor 3 ((D 0 THENA Auto))
          THEN RWO "finite-type-iff-list" 0
          THEN Auto
          THEN ExRepD
          THEN (InstConcl [⌜L⌝])⋅
          THEN Auto) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. SqStable(P[x])
4. L : {x:T| P[x]}  List
5. ∀x:{x:T| P[x]} . (x ∈ L)
6. x : T
7. P[x]
⊢ (x ∈ L)

2
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. SqStable(P[x])
4. L : {x:T| P[x]}  List
5. ∀x:{x:T| P[x]} . (x ∈ L)
6. x : T
7. (x ∈ L)
⊢ P[x]

3
.....wf..... 
1. T : Type
2. P : T ⟶ ℙ
3. ∀x:T. SqStable(P[x])
4. L : T List
5. ∀x:T. (P[x] ⇐⇒ (x ∈ L))
⊢ L ∈ {x:T| P[x]}  List

4
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. SqStable(P[x])
4. L : T List
5. ∀x:T. (P[x] ⇐⇒ (x ∈ L))
6. x : {x:T| P[x]} 
⊢ (x ∈ L)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:T.  SqStable(P[x]))  {}\mRightarrow{}  (finite-type(\{x:T|  P[x]\}  )  \mLeftarrow{}{}\mRightarrow{}  \mexists{}L:T  List.  \mforall{}x:T.  (P[x]  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))))


By

---

Latex:
TACTIC:(RepeatFor  3  ((D  0  THENA  Auto))
                THEN  RWO  "finite-type-iff-list"  0
                THEN  Auto
                THEN  ExRepD
                THEN  (InstConcl  [\mkleeneopen{}L\mkleeneclose{}])\mcdot{}
                THEN  Auto)

---

Home Index