---

Step * 1 of Lemma compose-fpf-dom


1. [A] : Type
2. [B] : A ─→ Type
3. f : x:A fp-> B[x]@i
4. [C] : Type
5. a : A ─→ (C?)@i
6. b : C ─→ A@i
7. y : C@i
⊢ (y ∈ fpf-domain(compose-fpf(a;b;f))) ⇐⇒ ∃x:A. ((x ∈ fpf-domain(f)) ∧ ((↑isl(a x)) c∧ (y = outl(a x) ∈ C)))
BY
{ (DVar `f' THEN RepUR ``fpf-domain compose-fpf`` 0) }

1
1. [A] : Type
2. [B] : A ─→ Type
3. d : A List@i
4. f1 : x:{x:A| (x ∈ d)}  ─→ B[x]@i
5. [C] : Type
6. a : A ─→ (C?)@i
7. b : C ─→ A@i
8. y : C@i
⊢ (y ∈ mapfilter(λx.outl(a x);λx.isl(a x);d)) ⇐⇒ ∃x:A. ((x ∈ d) ∧ ((↑isl(a x)) c∧ (y = outl(a x) ∈ C)))

---

Latex:



1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  f  :  x:A  fp->  B[x]@i
4.  [C]  :  Type
5.  a  :  A  {}\mrightarrow{}  (C?)@i
6.  b  :  C  {}\mrightarrow{}  A@i
7.  y  :  C@i
\mvdash{}  (y  \mmember{}  fpf-domain(compose-fpf(a;b;f)))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}x:A.  ((x  \mmember{}  fpf-domain(f))  \mwedge{}  ((\muparrow{}isl(a  x))  c\mwedge{}  (y  =  outl(a  x))))


By

(DVar  `f'  THEN  RepUR  ``fpf-domain  compose-fpf``  0)

---

Home Index