---

Step * 1 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])
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)
BY
{ (With ⌜f⌝ (D 0)⋅ THEN Auto THEN D 0 THEN Reduce 0 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]} 
12. a1 : ℕ||L||
13. a2 : ℕ||L||
14. (f a1) = (f a2) ∈ {y:B| P[y]} 
⊢ a1 = a2 ∈ ℕ||L||

---

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])
9.  f  :  i:\mBbbN{}||L||  {}\mrightarrow{}  B
10.  \mforall{}i:\mBbbN{}||L||.  (R[L[i];f  i]  \mwedge{}  P[f  i])
11.  f  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \{y:B|  P[y]\} 
\mvdash{}  \mexists{}f:\mBbbN{}||L||  {}\mrightarrow{}  \{y:B|  P[y]\}  .  Inj(\mBbbN{}||L||;\{y:B|  P[y]\}  ;f)


By

---

Latex:
(With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index