---

Step * 1 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]} 
12. a1 : ℕ||L||
13. a2 : ℕ||L||
14. (f a1) = (f a2) ∈ {y:B| P[y]} 
⊢ a1 = a2 ∈ ℕ||L||
BY
{ (InstHyp [⌜L[a1]⌝;⌜L[a2]⌝;⌜f a1⌝] 6⋅ 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]} 
15. L[a1] = L[a2] ∈ A
⊢ 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]\} 
12.  a1  :  \mBbbN{}||L||
13.  a2  :  \mBbbN{}||L||
14.  (f  a1)  =  (f  a2)
\mvdash{}  a1  =  a2


By

---

Latex:
(InstHyp  [\mkleeneopen{}L[a1]\mkleeneclose{};\mkleeneopen{}L[a2]\mkleeneclose{};\mkleeneopen{}f  a1\mkleeneclose{}]  6\mcdot{}  THEN  Auto)

---

Home Index