---

Step * of Lemma bag-settype

∀[T:Type]. ∀[bs:bag(T)]. ∀[P:T ⟶ ℙ].  bs ∈ bag({x:T| P[x]} ) supposing ∀x:T. (x ↓∈ bs ⇒ P[x])
BY
{ (Auto
   THEN newQuotD 2
   THEN (Assert a ∈ {x:T| P[x]}  List BY
               (BLemma `list-set-type2` THEN Auto THEN D 0 THEN Auto THEN BackThruSomeHyp THEN D 0 THEN Auto))) }

1
1. T : Type
2. T List ∈ Type
3. ∀as,b1:T List.  (permutation(T;as;b1) ∈ Type)
4. ∀as:T List. permutation(T;as;as)
5. a : Base
6. b : Base
7. c : a = b ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
8. a ∈ T List
9. b ∈ T List
10. permutation(T;a;b)
11. P : T ⟶ ℙ
12. ∀x:T. (x ↓∈ a ⇒ P[x])
13. a ∈ {x:T| P[x]}  List
⊢ a ∈ bag({x:T| P[x]} )

2
1. T : Type
2. T List ∈ Type
3. ∀as,b1:T List.  (permutation(T;as;b1) ∈ Type)
4. ∀as:T List. permutation(T;as;as)
5. a : Base
6. b : Base
7. c : a = b ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
8. a ∈ T List
9. b ∈ T List
10. permutation(T;a;b)
11. P : T ⟶ ℙ
12. ∀x:T. (x ↓∈ a ⇒ P[x])
13. a ∈ {x:T| P[x]}  List
⊢ a = b ∈ bag({x:T| P[x]} )

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    bs  \mmember{}  bag(\{x:T|  P[x]\}  )  supposing  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  P[x])


By

---

Latex:
(Auto
  THEN  newQuotD  2
  THEN  (Assert  a  \mmember{}  \{x:T|  P[x]\}    List  BY
                          (BLemma  `list-set-type2`
                            THEN  Auto
                            THEN  D  0
                            THEN  Auto
                            THEN  BackThruSomeHyp
                            THEN  D  0
                            THEN  Auto)))

---

Home Index