---

Step * 1 of Lemma equipollent-nat-powered2


1. g : ∀n:ℕ. ∃f:ℕ ⟶ (ℕ^n + 1). Bij(ℕ;(ℕ^n + 1);f)
⊢ ∃f:n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1). ∀n:ℕ. Bij(ℕ;(ℕ^n + 1);f n)
BY
{ (InstConcl [⌜λn.(fst((g n)))⌝]⋅ THEN Auto THEN Reduce 0 THEN GenConclAtAddr [3;1] THEN DVar `v') }

1
1. g : ∀n:ℕ. ∃f:ℕ ⟶ (ℕ^n + 1). Bij(ℕ;(ℕ^n + 1);f)
2. n : ℕ@i
3. f : ℕ ⟶ (ℕ^n + 1)@i
4. v1 : Bij(ℕ;(ℕ^n + 1);f)@i
5. (g n) = <f, v1> ∈ (∃f:ℕ ⟶ (ℕ^n + 1). Bij(ℕ;(ℕ^n + 1);f))@i
⊢ Bij(ℕ;(ℕ^n + 1);fst(<f, v1>))

---

Latex:

---

Latex:

1.  g  :  \mforall{}n:\mBbbN{}.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1).  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);f)
\mvdash{}  \mexists{}f:n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1).  \mforall{}n:\mBbbN{}.  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);f  n)


By

---

Latex:
(InstConcl  [\mkleeneopen{}\mlambda{}n.(fst((g  n)))\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  GenConclAtAddr  [3;1]  THEN  DVar  `v')

---

Home Index