---

Step * 2 1 1 1 1 1 1 1 of Lemma bag-intersection


1. n : ℕ
2. m : ℕ
3. p : ℕ
4. q : ℕ
5. f : ℕp + q ⟶ ℕn + m
6. (p + q) = (n + m) ∈ ℤ
7. m < n
8. q < p
9. ∀i:ℕp. (n ≤ f[i])
10. a1 : ℕp
11. a2 : ℕp
12. (f a1) = (f a2) ∈ {n..n + m-}
13. ∀a2:ℕp + q. (((f a1) = (f a2) ∈ ℕn + m) ⇒ (a1 = a2 ∈ ℕp + q))
⊢ a1 = a2 ∈ ℕp
BY
{ (InstHyp [⌜a2⌝] (-1)⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  p  :  \mBbbN{}
4.  q  :  \mBbbN{}
5.  f  :  \mBbbN{}p  +  q  {}\mrightarrow{}  \mBbbN{}n  +  m
6.  (p  +  q)  =  (n  +  m)
7.  m  <  n
8.  q  <  p
9.  \mforall{}i:\mBbbN{}p.  (n  \mleq{}  f[i])
10.  a1  :  \mBbbN{}p
11.  a2  :  \mBbbN{}p
12.  (f  a1)  =  (f  a2)
13.  \mforall{}a2:\mBbbN{}p  +  q.  (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))
\mvdash{}  a1  =  a2


By

---

Latex:
(InstHyp  [\mkleeneopen{}a2\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto')

---

Home Index