---

Step * 1 of Lemma l_all_exists_injection


1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ B ⟶ ℙ
4. [P] : B ⟶ ℙ
5. L : A List
6. ∀x1,x2:A. ∀y:B.  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ A))
7. no_repeats(A;L)
8. ∀i:ℕ||L||. ∃y:B. (R[L[i];y] ∧ P[y])
⊢ ∃f:ℕ||L|| ⟶ {y:B| P[y]} . Inj(ℕ||L||;{y:B| P[y]} ;f)
BY
{ ((Skolemize (-1) `f' THEN Auto)
   THEN (Assert f ∈ ℕ||L|| ⟶ {y:B| P[y]}  BY
               (ExtWith [`z'] [⌜i:ℕ||L|| ⟶ B⌝]⋅ THEN Auto))
   ) }

1
1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ B ⟶ ℙ
4. [P] : B ⟶ ℙ
5. L : A List
6. ∀x1,x2:A. ∀y:B.  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ A))
7. no_repeats(A;L)
8. ∀i:ℕ||L||. ∃y:B. (R[L[i];y] ∧ P[y])
9. f : i:ℕ||L|| ⟶ B
10. ∀i:ℕ||L||. (R[L[i];f i] ∧ P[f i])
11. f ∈ ℕ||L|| ⟶ {y:B| P[y]} 
⊢ ∃f:ℕ||L|| ⟶ {y:B| P[y]} . Inj(ℕ||L||;{y:B| P[y]} ;f)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [R]  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
4.  [P]  :  B  {}\mrightarrow{}  \mBbbP{}
5.  L  :  A  List
6.  \mforall{}x1,x2:A.  \mforall{}y:B.    (R[x1;y]  {}\mRightarrow{}  R[x2;y]  {}\mRightarrow{}  (x1  =  x2))
7.  no\_repeats(A;L)
8.  \mforall{}i:\mBbbN{}||L||.  \mexists{}y:B.  (R[L[i];y]  \mwedge{}  P[y])
\mvdash{}  \mexists{}f:\mBbbN{}||L||  {}\mrightarrow{}  \{y:B|  P[y]\}  .  Inj(\mBbbN{}||L||;\{y:B|  P[y]\}  ;f)


By

---

Latex:
((Skolemize  (-1)  `f'  THEN  Auto)
  THEN  (Assert  f  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \{y:B|  P[y]\}    BY
                          (ExtWith  [`z']  [\mkleeneopen{}i:\mBbbN{}||L||  {}\mrightarrow{}  B\mkleeneclose{}]\mcdot{}  THEN  Auto))
  )

---

Home Index