---

Step * 1 1 1 1 of Lemma fpf-union-contains2

.....equality..... 
1. A : Type
2. V : Type
3. B : A ─→ Type
4. ∀a:A. ((B a) ⊆r V)
5. eq : EqDecider(A)@i
6. f : x:A fp-> (B x) List@i
7. g : x:A fp-> (B x) List@i
8. fpf-single-valued(A;eq;x.B x;V;g)
9. x : A@i
10. R : (V List) ─→ V ─→ 𝔹@i
11. ∀x:A
      ((↑x ∈ dom(g))
      ⇒ (↑x ∈ dom(f))
      ⇒ (∀a:V
            ((((a ∈ g(x)) ∧ (¬↑(R f(x) a))) ∨ ((a ∈ f(x)) ∧ (¬↑(R g(x) a))))
            ⇒ (∃a':B x. ((a' = a ∈ V) ∧ (a' ∈ f(x)) ∧ (a' ∈ g(x)))))))@i
12. ↑x ∈ dom(g)
13. ↑x ∈ dom(f)
14. (B x) ⊆r V
15. a : B x@i
16. (a ∈ g(x))@i
17. ¬↑(R f(x) a)
18. a' : B x
19. a' = a ∈ V
20. (a' ∈ f(x))
21. (a' ∈ g(x))
⊢ a = a' ∈ B[x]
BY
{ (All (Unfold `so_apply`)  THEN Auto) }

---

Latex:


.....equality..... 
1.  A  :  Type
2.  V  :  Type
3.  B  :  A  {}\mrightarrow{}  Type
4.  \mforall{}a:A.  ((B  a)  \msubseteq{}r  V)
5.  eq  :  EqDecider(A)@i
6.  f  :  x:A  fp->  (B  x)  List@i
7.  g  :  x:A  fp->  (B  x)  List@i
8.  fpf-single-valued(A;eq;x.B  x;V;g)
9.  x  :  A@i
10.  R  :  (V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}@i
11.  \mforall{}x:A
            ((\muparrow{}x  \mmember{}  dom(g))
            {}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))
            {}\mRightarrow{}  (\mforall{}a:V
                        ((((a  \mmember{}  g(x))  \mwedge{}  (\mneg{}\muparrow{}(R  f(x)  a)))  \mvee{}  ((a  \mmember{}  f(x))  \mwedge{}  (\mneg{}\muparrow{}(R  g(x)  a))))
                        {}\mRightarrow{}  (\mexists{}a':B  x.  ((a'  =  a)  \mwedge{}  (a'  \mmember{}  f(x))  \mwedge{}  (a'  \mmember{}  g(x)))))))@i
12.  \muparrow{}x  \mmember{}  dom(g)
13.  \muparrow{}x  \mmember{}  dom(f)
14.  (B  x)  \msubseteq{}r  V
15.  a  :  B  x@i
16.  (a  \mmember{}  g(x))@i
17.  \mneg{}\muparrow{}(R  f(x)  a)
18.  a'  :  B  x
19.  a'  =  a
20.  (a'  \mmember{}  f(x))
21.  (a'  \mmember{}  g(x))
\mvdash{}  a  =  a'


By

(All  (Unfold  `so\_apply`)    THEN  Auto)

---

Home Index