Step * 2 of Lemma singlevalued-graph-iff


1. coSet{i:l}
2. {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. 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)
BY
(Unfold `singlevalued-graph` THEN (BLemma `implies-allsetmem` THENA Auto)) }

1
1. coSet{i:l}
2. {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. 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))
⊢ ∀a:coSet{i:l}. ((a ∈ A)  ∀b1∈B[a].∀b2∈B[a].((a,b1) ∈ x)  ((a,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,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))
\mvdash{}  singlevalued-graph(A;a.B[a];x)


By


Latex:
(Unfold  `singlevalued-graph`  0  THEN  (BLemma  `implies-allsetmem`  THENA  Auto))




Home Index