---

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


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∈A.∀b1∈B[a].∀b2∈B[a].((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2)
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)
14. a1 : coSet{i:l}
15. a2 : coSet{i:l}
16. (a1 ∈ A)
17. (a2 ∈ A)
18. seteq(a1;a2)
19. ∀b1:coSet{i:l}. ((b1 ∈ B[a1]) ⇒ ∀b2∈B[a1].((a1,b1) ∈ x) ⇒ ((a1,b2) ∈ x) ⇒ seteq(b1;b2))
⊢ ∀b1∈B[a2].∀b2∈B[a2].((a2,b1) ∈ x) ⇒ ((a2,b2) ∈ x) ⇒ seteq(b1;b2)
BY
{ (RWO "allsetmem-iff" 0 THENA 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. ∀a∈A.∀b1∈B[a].∀b2∈B[a].((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2)
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)
14. a1 : coSet{i:l}
15. a2 : coSet{i:l}
16. (a1 ∈ A)
17. (a2 ∈ A)
18. seteq(a1;a2)
19. ∀b1:coSet{i:l}. ((b1 ∈ B[a1]) ⇒ ∀b2∈B[a1].((a1,b1) ∈ x) ⇒ ((a1,b2) ∈ x) ⇒ seteq(b1;b2))
⊢ ∀b1:coSet{i:l}. ((b1 ∈ B[a2]) ⇒ ∀b2∈B[a2].((a2,b1) ∈ x) ⇒ ((a2,b2) ∈ x) ⇒ seteq(b1;b2))

---

Latex:

---

Latex:

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\mmember{}A.\mforall{}b1\mmember{}B[a].\mforall{}b2\mmember{}B[a].((a,b1)  \mmember{}  x)  {}\mRightarrow{}  ((a,b2)  \mmember{}  x)  {}\mRightarrow{}  seteq(b1;b2)
6.  a  :  coSet\{i:l\}
7.  b1  :  coSet\{i:l\}
8.  b2  :  coSet\{i:l\}
9.  (a  \mmember{}  A)
10.  (b1  \mmember{}  B[a])
11.  (b2  \mmember{}  B[a])
12.  ((a,b1)  \mmember{}  x)
13.  ((a,b2)  \mmember{}  x)
14.  a1  :  coSet\{i:l\}
15.  a2  :  coSet\{i:l\}
16.  (a1  \mmember{}  A)
17.  (a2  \mmember{}  A)
18.  seteq(a1;a2)
19.  \mforall{}b1:coSet\{i:l\}.  ((b1  \mmember{}  B[a1])  {}\mRightarrow{}  \mforall{}b2\mmember{}B[a1].((a1,b1)  \mmember{}  x)  {}\mRightarrow{}  ((a1,b2)  \mmember{}  x)  {}\mRightarrow{}  seteq(b1;b2))
\mvdash{}  \mforall{}b1\mmember{}B[a2].\mforall{}b2\mmember{}B[a2].((a2,b1)  \mmember{}  x)  {}\mRightarrow{}  ((a2,b2)  \mmember{}  x)  {}\mRightarrow{}  seteq(b1;b2)


By

---

Latex:
(RWO  "allsetmem-iff"  0  THENA  Auto)

---

Home Index