---

Step * of Lemma fpf-cap_functionality_wrt_sub

∀[A:Type]. ∀[d1,d2,d3,d4:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[f,g:a:A fp-> B[a]]. ∀[x:A]. ∀[z:B[x]].
  (f(x)?z = g(x)?z ∈ B[x]) supposing ((↑x ∈ dom(f)) and f ⊆ g)
BY
{ (Auto THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE THEN Auto THEN SplitOnConclITE THEN Auto) }

1
.....truecase..... 
1. A : Type
2. d1 : EqDecider(A)
3. d2 : EqDecider(A)
4. d3 : EqDecider(A)
5. d4 : EqDecider(A)
6. B : A ─→ Type
7. f : a:A fp-> B[a]
8. g : a:A fp-> B[a]
9. x : A
10. z : B[x]
11. f ⊆ g
12. ↑x ∈ dom(f)
13. ↑x ∈ dom(f)
14. ↑x ∈ dom(g)
⊢ f(x) = g(x) ∈ B[x]

2
.....falsecase..... 
1. A : Type
2. d1 : EqDecider(A)
3. d2 : EqDecider(A)
4. d3 : EqDecider(A)
5. d4 : EqDecider(A)
6. B : A ─→ Type
7. f : a:A fp-> B[a]
8. g : a:A fp-> B[a]
9. x : A
10. z : B[x]
11. f ⊆ g
12. ↑x ∈ dom(f)
13. ↑x ∈ dom(f)
14. ¬↑x ∈ dom(g)
⊢ f(x) = z ∈ B[x]

3
.....truecase..... 
1. A : Type
2. d1 : EqDecider(A)
3. d2 : EqDecider(A)
4. d3 : EqDecider(A)
5. d4 : EqDecider(A)
6. B : A ─→ Type
7. f : a:A fp-> B[a]
8. g : a:A fp-> B[a]
9. x : A
10. z : B[x]
11. f ⊆ g
12. ↑x ∈ dom(f)
13. ¬↑x ∈ dom(f)
14. ↑x ∈ dom(g)
⊢ z = g(x) ∈ B[x]

---

Latex:


\mforall{}[A:Type].  \mforall{}[d1,d2,d3,d4:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f,g:a:A  fp->  B[a]].  \mforall{}[x:A].  \mforall{}[z:B[x]].
    (f(x)?z  =  g(x)?z)  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  f  \msubseteq{}  g)


By

(Auto  THEN  Unfold  `fpf-cap`  0  THEN  SplitOnConclITE  THEN  Auto  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index