---

Step * 1 of Lemma compose-fpf-dom


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

1
1. [A] : Type
2. [B] : A ⟶ Type
3. d : A List
4. f1 : x:{x:A| (x ∈ d)}  ⟶ B[x]
5. [C] : Type
6. a : A ⟶ (C?)
7. b : C ⟶ A
8. y : C
⊢ (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:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  f  :  x:A  fp->  B[x]
4.  [C]  :  Type
5.  a  :  A  {}\mrightarrow{}  (C?)
6.  b  :  C  {}\mrightarrow{}  A
7.  y  :  C
\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

---

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

---

Home Index