---

Step * 2 1 1 1 1 1 of Lemma singlevalued-graph-iff

.....rewrite subgoal..... 
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))
6. a : coSet{i:l}
7. ∀b1,b2:coSet{i:l}.  ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
8. (a ∈ A)
9. b1 : coSet{i:l}
10. ∀b2:coSet{i:l}. ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
11. (b1 ∈ B[a])
⊢ set-predicate{i:l}(B[a];b2.((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
BY
{ (D 0 THEN Auto) }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  A  :  coSet\{i:l\}
2.  B  :  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}
3.  \mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  A)  {}\mRightarrow{}  (a2  \mmember{}  A)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  seteq(B[a1];B[a2]))
4.  x  :  coSet\{i:l\}
5.  \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))
6.  a  :  coSet\{i:l\}
7.  \mforall{}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))
8.  (a  \mmember{}  A)
9.  b1  :  coSet\{i:l\}
10.  \mforall{}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))
11.  (b1  \mmember{}  B[a])
\mvdash{}  set-predicate\{i:l\}(B[a];b2.((a,b1)  \mmember{}  x)  {}\mRightarrow{}  ((a,b2)  \mmember{}  x)  {}\mRightarrow{}  seteq(b1;b2))


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index