---

Step * of Lemma compose-fpf-dom

∀[A:Type]. ∀[B:A ─→ Type].
  ∀f:x:A fp-> B[x]
    ∀[C:Type]
      ∀a:A ─→ (C?). ∀b:C ─→ A. ∀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
{ (UnivCD THENA Auto) }

1
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)))

---

Latex:


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

(UnivCD  THENA  Auto)

---

Home Index