---

Step * 2 1 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. 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)))
BY
{ (D 0 With ⌜y⌝  THEN Auto THEN Unfold `fset-member` -3 THEN RW  assert_pushdownC (-3) THEN Auto) }

---

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.  istype(T  List)
8.  \mforall{}x1,y1:T  List.    istype(set-equal(T;x1;y1))
9.  \mforall{}x1:T  List.  set-equal(T;x1;x1)
10.  a  :  Base
11.  b  :  Base
12.  c  :  a  =  b
13.  a  \mmember{}  T  List
14.  b  \mmember{}  T  List
15.  set-equal(T;a;b)
16.  x  :  X
17.  y  :  T
18.  y  \mmember{}  a
19.  \muparrow{}(P  y)
20.  x  =  (f  y)
\mvdash{}  \mexists{}y:T.  ((y  \mmember{}  a)  \mwedge{}  ((\muparrow{}(P  y))  c\mwedge{}  (x  =  (f  y))))


By

---

Latex:
(D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto  THEN  Unfold  `fset-member`  -3  THEN  RW    assert\_pushdownC  (-3)  THEN  Auto)

---

Home Index