Step | Hyp | Ref
| Expression |
1 | | structtousgr.p |
. . 3
β’ π = {π₯ β π« (Baseβπ) β£ (β―βπ₯) = 2} |
2 | | structtousgr.s |
. . 3
β’ (π β π Struct π) |
3 | | structtousgr.g |
. . 3
β’ πΊ = (π sSet β¨(.efβndx), ( I βΎ
π)β©) |
4 | | structtousgr.b |
. . 3
β’ (π β (Baseβndx) β
dom π) |
5 | 1, 2, 3, 4 | structtousgr 28702 |
. 2
β’ (π β πΊ β USGraph) |
6 | | simpr 486 |
. . . . 5
β’ ((π β§ π£ β (VtxβπΊ)) β π£ β (VtxβπΊ)) |
7 | | eldifi 4127 |
. . . . . . . 8
β’ (π β ((VtxβπΊ) β {π£}) β π β (VtxβπΊ)) |
8 | 6, 7 | anim12ci 615 |
. . . . . . 7
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β (π β (VtxβπΊ) β§ π£ β (VtxβπΊ))) |
9 | | eldifsni 4794 |
. . . . . . . 8
β’ (π β ((VtxβπΊ) β {π£}) β π β π£) |
10 | 9 | adantl 483 |
. . . . . . 7
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β π β π£) |
11 | | fvexd 6907 |
. . . . . . . . 9
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β (Baseβπ) β V) |
12 | 3 | fveq2i 6895 |
. . . . . . . . . . . . 13
β’
(VtxβπΊ) =
(Vtxβ(π sSet
β¨(.efβndx), ( I βΎ π)β©)) |
13 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(.efβndx) = (.efβndx) |
14 | | fvex 6905 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ)
β V |
15 | 1 | cusgrexilem1 28696 |
. . . . . . . . . . . . . . 15
β’
((Baseβπ)
β V β ( I βΎ π) β V) |
16 | 14, 15 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ (π β ( I βΎ π) β V) |
17 | 13, 2, 4, 16 | setsvtx 28295 |
. . . . . . . . . . . . 13
β’ (π β (Vtxβ(π sSet β¨(.efβndx), ( I
βΎ π)β©)) =
(Baseβπ)) |
18 | 12, 17 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ (π β (VtxβπΊ) = (Baseβπ)) |
19 | 18 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π β (π£ β (VtxβπΊ) β π£ β (Baseβπ))) |
20 | 19 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ π£ β (VtxβπΊ)) β π£ β (Baseβπ)) |
21 | 20 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β π£ β (Baseβπ)) |
22 | 18 | difeq1d 4122 |
. . . . . . . . . . . . 13
β’ (π β ((VtxβπΊ) β {π£}) = ((Baseβπ) β {π£})) |
23 | 22 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π β (π β ((VtxβπΊ) β {π£}) β π β ((Baseβπ) β {π£}))) |
24 | 23 | biimpd 228 |
. . . . . . . . . . 11
β’ (π β (π β ((VtxβπΊ) β {π£}) β π β ((Baseβπ) β {π£}))) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π£ β (VtxβπΊ)) β (π β ((VtxβπΊ) β {π£}) β π β ((Baseβπ) β {π£}))) |
26 | 25 | imp 408 |
. . . . . . . . 9
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β π β ((Baseβπ) β {π£})) |
27 | 1 | cusgrexilem2 28699 |
. . . . . . . . 9
β’
((((Baseβπ)
β V β§ π£ β
(Baseβπ)) β§ π β ((Baseβπ) β {π£})) β βπ β ran ( I βΎ π){π£, π} β π) |
28 | 11, 21, 26, 27 | syl21anc 837 |
. . . . . . . 8
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β βπ β ran ( I βΎ π){π£, π} β π) |
29 | | edgval 28309 |
. . . . . . . . . . 11
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
30 | 3 | fveq2i 6895 |
. . . . . . . . . . . . 13
β’
(iEdgβπΊ) =
(iEdgβ(π sSet
β¨(.efβndx), ( I βΎ π)β©)) |
31 | 13, 2, 4, 16 | setsiedg 28296 |
. . . . . . . . . . . . 13
β’ (π β (iEdgβ(π sSet β¨(.efβndx), ( I
βΎ π)β©)) = ( I
βΎ π)) |
32 | 30, 31 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ (π β (iEdgβπΊ) = ( I βΎ π)) |
33 | 32 | rneqd 5938 |
. . . . . . . . . . 11
β’ (π β ran (iEdgβπΊ) = ran ( I βΎ π)) |
34 | 29, 33 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β (EdgβπΊ) = ran ( I βΎ π)) |
35 | 34 | rexeqdv 3327 |
. . . . . . . . 9
β’ (π β (βπ β (EdgβπΊ){π£, π} β π β βπ β ran ( I βΎ π){π£, π} β π)) |
36 | 35 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β (βπ β (EdgβπΊ){π£, π} β π β βπ β ran ( I βΎ π){π£, π} β π)) |
37 | 28, 36 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β βπ β (EdgβπΊ){π£, π} β π) |
38 | | eqid 2733 |
. . . . . . . 8
β’
(VtxβπΊ) =
(VtxβπΊ) |
39 | | eqid 2733 |
. . . . . . . 8
β’
(EdgβπΊ) =
(EdgβπΊ) |
40 | 38, 39 | nbgrel 28597 |
. . . . . . 7
β’ (π β (πΊ NeighbVtx π£) β ((π β (VtxβπΊ) β§ π£ β (VtxβπΊ)) β§ π β π£ β§ βπ β (EdgβπΊ){π£, π} β π)) |
41 | 8, 10, 37, 40 | syl3anbrc 1344 |
. . . . . 6
β’ (((π β§ π£ β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π£})) β π β (πΊ NeighbVtx π£)) |
42 | 41 | ralrimiva 3147 |
. . . . 5
β’ ((π β§ π£ β (VtxβπΊ)) β βπ β ((VtxβπΊ) β {π£})π β (πΊ NeighbVtx π£)) |
43 | 38 | uvtxel 28645 |
. . . . 5
β’ (π£ β (UnivVtxβπΊ) β (π£ β (VtxβπΊ) β§ βπ β ((VtxβπΊ) β {π£})π β (πΊ NeighbVtx π£))) |
44 | 6, 42, 43 | sylanbrc 584 |
. . . 4
β’ ((π β§ π£ β (VtxβπΊ)) β π£ β (UnivVtxβπΊ)) |
45 | 44 | ralrimiva 3147 |
. . 3
β’ (π β βπ£ β (VtxβπΊ)π£ β (UnivVtxβπΊ)) |
46 | 5 | elexd 3495 |
. . . 4
β’ (π β πΊ β V) |
47 | 38 | iscplgr 28672 |
. . . 4
β’ (πΊ β V β (πΊ β ComplGraph β
βπ£ β
(VtxβπΊ)π£ β (UnivVtxβπΊ))) |
48 | 46, 47 | syl 17 |
. . 3
β’ (π β (πΊ β ComplGraph β βπ£ β (VtxβπΊ)π£ β (UnivVtxβπΊ))) |
49 | 45, 48 | mpbird 257 |
. 2
β’ (π β πΊ β ComplGraph) |
50 | | iscusgr 28675 |
. 2
β’ (πΊ β ComplUSGraph β
(πΊ β USGraph β§
πΊ β
ComplGraph)) |
51 | 5, 49, 50 | sylanbrc 584 |
1
β’ (π β πΊ β ComplUSGraph) |