---

Step * 2 1 of Lemma member-fset-mapfilter


1. T : Type
2. eqT : EqDecider(T)
3. P : T ⟶ 𝔹
4. X : Type
5. eqX : EqDecider(X)
6. f : {x:T| ↑(P x)}  ⟶ X
7. s : fset(T)
8. x : X
9. y : T
10. y ∈ s
11. ↑(P y)
12. x = (f y) ∈ X
13. ¬x ∈ fset-mapfilter(f;P;s)
⊢ 0 = 1 ∈ ℤ
BY
{ (Dquotient2 7
   THEN D -1
   THEN Unfold `fset-mapfilter` 0
   THEN Unfold `fset-member` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN BLemma `member-mapfilter`
   THEN Auto) }

1
1. T : Type
2. eqT : EqDecider(T)
3. P : T ⟶ 𝔹
4. X : Type
5. eqX : EqDecider(X)
6. f : {x:T| ↑(P x)}  ⟶ X
7. istype(T List)
8. ∀x1,y1:T List.  istype(set-equal(T;x1;y1))
9. ∀x1:T List. set-equal(T;x1;x1)
10. a : Base
11. b : Base
12. c : a = b ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
13. a ∈ T List
14. b ∈ T List
15. set-equal(T;a;b)
16. x : X
17. y : T
18. y ∈ a
19. ↑(P y)
20. x = (f y) ∈ X
⊢ ∃y:T. ((y ∈ a) ∧ ((↑(P y)) c∧ (x = (f y) ∈ X)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eqT  :  EqDecider(T)
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
4.  X  :  Type
5.  eqX  :  EqDecider(X)
6.  f  :  \{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  X
7.  s  :  fset(T)
8.  x  :  X
9.  y  :  T
10.  y  \mmember{}  s
11.  \muparrow{}(P  y)
12.  x  =  (f  y)
13.  \mneg{}x  \mmember{}  fset-mapfilter(f;P;s)
\mvdash{}  0  =  1


By

---

Latex:
(Dquotient2  7
  THEN  D  -1
  THEN  Unfold  `fset-mapfilter`  0
  THEN  Unfold  `fset-member`  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  BLemma  `member-mapfilter`
  THEN  Auto)

---

Home Index