---

Step * of Lemma singlevalued-graph-iff

No Annotations
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
  ⇒ (∀x:coSet{i:l}
        (singlevalued-graph(A;a.B[a];x)
        ⇐⇒ ∀a,b1,b2:coSet{i:l}.
              ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2)))))
BY
{ Auto }

1
1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. ∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
4. x : coSet{i:l}
5. singlevalued-graph(A;a.B[a];x)
6. a : coSet{i:l}
7. b1 : coSet{i:l}
8. b2 : coSet{i:l}
9. (a ∈ A)
10. (b1 ∈ B[a])
11. (b2 ∈ B[a])
12. ((a,b1) ∈ x)
13. ((a,b2) ∈ x)
⊢ seteq(b1;b2)

2
1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. ∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
4. x : coSet{i:l}
5. ∀a,b1,b2:coSet{i:l}.  ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
⊢ singlevalued-graph(A;a.B[a];x)

---

Latex:

---

Latex:
No  Annotations
\mforall{}A:coSet\{i:l\}.  \mforall{}B:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}.
    ((\mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  A)  {}\mRightarrow{}  (a2  \mmember{}  A)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  seteq(B[a1];B[a2])))
    {}\mRightarrow{}  (\mforall{}x:coSet\{i:l\}
                (singlevalued-graph(A;a.B[a];x)
                \mLeftarrow{}{}\mRightarrow{}  \mforall{}a,b1,b2:coSet\{i:l\}.
                            ((a  \mmember{}  A)
                            {}\mRightarrow{}  (b1  \mmember{}  B[a])
                            {}\mRightarrow{}  (b2  \mmember{}  B[a])
                            {}\mRightarrow{}  ((a,b1)  \mmember{}  x)
                            {}\mRightarrow{}  ((a,b2)  \mmember{}  x)
                            {}\mRightarrow{}  seteq(b1;b2)))))


By

---

Latex:
Auto

---

Home Index