---

Step * 1 1 1 of Lemma not-all-finite


1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. k : ℕ
5. f : T ⟶ ℕk
6. Inj(T;ℕk;f)
7. ∀b:ℕk. ∃a:T. ((f a) = b ∈ ℕk)
8. g : b:ℕk ⟶ T
9. ∀b:ℕk. ((f (g b)) = b ∈ ℕk)
10. ∀x:ℕk. P[g x]
11. x : T
⊢ P[x]
BY
{ ((InstHyp [⌜f x⌝] (-2)⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. T : Type
2. P : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. k : ℕ
5. f : T ⟶ ℕk
6. Inj(T;ℕk;f)
7. ∀b:ℕk. ∃a:T. ((f a) = b ∈ ℕk)
8. g : b:ℕk ⟶ T
9. ∀b:ℕk. ((f (g b)) = b ∈ ℕk)
10. ∀x:ℕk. P[g x]
11. x : T
12. P[g (f x)]
⊢ x = (g (f x)) ∈ T

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  Dec(P[x])
4.  k  :  \mBbbN{}
5.  f  :  T  {}\mrightarrow{}  \mBbbN{}k
6.  Inj(T;\mBbbN{}k;f)
7.  \mforall{}b:\mBbbN{}k.  \mexists{}a:T.  ((f  a)  =  b)
8.  g  :  b:\mBbbN{}k  {}\mrightarrow{}  T
9.  \mforall{}b:\mBbbN{}k.  ((f  (g  b))  =  b)
10.  \mforall{}x:\mBbbN{}k.  P[g  x]
11.  x  :  T
\mvdash{}  P[x]


By

---

Latex:
((InstHyp  [\mkleeneopen{}f  x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCDA)

---

Home Index