Step
*
3
1
1
of Lemma
bag-member-product
1. A : Type
2. B : Type
3. bs : bag(B)
4. p1 : A
5. p2 : B
6. u : A
7. v : A List
8. p1 ↓∈ v ∧ p2 ↓∈ bs supposing <p1, p2> ↓∈ v × bs
9. <p1, p2> ↓∈ v × bs supposing p1 ↓∈ v ∧ p2 ↓∈ bs
10. p1 = u ∈ A
11. p2 ↓∈ bs
⊢ ↓∃v:B. (v ↓∈ bs ∧ (<p1, p2> = <u, v> ∈ (A × B)))
BY
{ (D 0 THEN Auto) }
Latex:
Latex:
1. A : Type
2. B : Type
3. bs : bag(B)
4. p1 : A
5. p2 : B
6. u : A
7. v : A List
8. p1 \mdownarrow{}\mmember{} v \mwedge{} p2 \mdownarrow{}\mmember{} bs supposing <p1, p2> \mdownarrow{}\mmember{} v \mtimes{} bs
9. <p1, p2> \mdownarrow{}\mmember{} v \mtimes{} bs supposing p1 \mdownarrow{}\mmember{} v \mwedge{} p2 \mdownarrow{}\mmember{} bs
10. p1 = u
11. p2 \mdownarrow{}\mmember{} bs
\mvdash{} \mdownarrow{}\mexists{}v:B. (v \mdownarrow{}\mmember{} bs \mwedge{} (<p1, p2> = <u, v>))
By
Latex:
(D 0 THEN Auto)
Home
Index