---

Step * 2 1 of Lemma fpf-contains-union-join-left2


1. [A] : Type
2. [B] : A ⟶ Type
3. eq : EqDecider(A)
4. f : a:A fp-> B[a] List
5. h : a:A fp-> B[a] List
6. g : a:A fp-> B[a] List
7. R : ⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹)
8. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)))
9. x : A
10. ↑x ∈ dom(h)
11. ↑x ∈ dom(f)
12. ∀i:ℕ||h(x)||. (h(x)[i] ∈ f(x))
13. i : ℕ||h(x)||
14. (h(x)[i] ∈ f(x))
15. ∀a:B[x]. ((a ∈ f(x)?[]) ⇒ (a ∈ fpf-union(f;g;eq;R;x)))
⊢ (h(x)[i] ∈ f(x)?[])
BY
{ (Unfold `fpf-cap` 0 THEN SplitOnConclITE THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  eq  :  EqDecider(A)
4.  f  :  a:A  fp->  B[a]  List
5.  h  :  a:A  fp->  B[a]  List
6.  g  :  a:A  fp->  B[a]  List
7.  R  :  \mcap{}a:A.  ((B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{})
8.  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(h))  {}\mRightarrow{}  ((\muparrow{}x  \mmember{}  dom(f))  c\mwedge{}  h(x)  \msubseteq{}  f(x)))
9.  x  :  A
10.  \muparrow{}x  \mmember{}  dom(h)
11.  \muparrow{}x  \mmember{}  dom(f)
12.  \mforall{}i:\mBbbN{}||h(x)||.  (h(x)[i]  \mmember{}  f(x))
13.  i  :  \mBbbN{}||h(x)||
14.  (h(x)[i]  \mmember{}  f(x))
15.  \mforall{}a:B[x].  ((a  \mmember{}  f(x)?[])  {}\mRightarrow{}  (a  \mmember{}  fpf-union(f;g;eq;R;x)))
\mvdash{}  (h(x)[i]  \mmember{}  f(x)?[])


By

---

Latex:
(Unfold  `fpf-cap`  0  THEN  SplitOnConclITE  THEN  Auto)\mcdot{}

---

Home Index