# Metamath Proof Explorer

## Theorem structtocusgr

Description: Any (extensible) structure with a base set can be made a complete simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021) (Revised by AV, 17-Nov-2021) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypotheses structtousgr.p ${⊢}{P}=\left\{{x}\in 𝒫{\mathrm{Base}}_{{S}}|\left|{x}\right|=2\right\}$
structtousgr.s ${⊢}{\phi }\to {S}\mathrm{Struct}{X}$
structtousgr.g ${⊢}{G}={S}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}↾}_{{P}}⟩$
structtousgr.b ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{S}$
Assertion structtocusgr ${⊢}{\phi }\to {G}\in \mathrm{ComplUSGraph}$

### Proof

Step Hyp Ref Expression
1 structtousgr.p ${⊢}{P}=\left\{{x}\in 𝒫{\mathrm{Base}}_{{S}}|\left|{x}\right|=2\right\}$
2 structtousgr.s ${⊢}{\phi }\to {S}\mathrm{Struct}{X}$
3 structtousgr.g ${⊢}{G}={S}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}↾}_{{P}}⟩$
4 structtousgr.b ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{S}$
5 1 2 3 4 structtousgr ${⊢}{\phi }\to {G}\in \mathrm{USGraph}$
6 simpr ${⊢}\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\to {v}\in \mathrm{Vtx}\left({G}\right)$
7 eldifi ${⊢}{n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\to {n}\in \mathrm{Vtx}\left({G}\right)$
8 6 7 anim12ci ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to \left({n}\in \mathrm{Vtx}\left({G}\right)\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)$
9 eldifsni ${⊢}{n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\to {n}\ne {v}$
10 9 adantl ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to {n}\ne {v}$
11 fvexd ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to {\mathrm{Base}}_{{S}}\in \mathrm{V}$
12 3 fveq2i ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({S}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}↾}_{{P}}⟩\right)$
13 eqid ${⊢}\mathrm{ef}\left(\mathrm{ndx}\right)=\mathrm{ef}\left(\mathrm{ndx}\right)$
14 fvex ${⊢}{\mathrm{Base}}_{{S}}\in \mathrm{V}$
15 1 cusgrexilem1 ${⊢}{\mathrm{Base}}_{{S}}\in \mathrm{V}\to {\mathrm{I}↾}_{{P}}\in \mathrm{V}$
16 14 15 mp1i ${⊢}{\phi }\to {\mathrm{I}↾}_{{P}}\in \mathrm{V}$
17 13 2 4 16 setsvtx ${⊢}{\phi }\to \mathrm{Vtx}\left({S}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}↾}_{{P}}⟩\right)={\mathrm{Base}}_{{S}}$
18 12 17 syl5eq ${⊢}{\phi }\to \mathrm{Vtx}\left({G}\right)={\mathrm{Base}}_{{S}}$
19 18 eleq2d ${⊢}{\phi }\to \left({v}\in \mathrm{Vtx}\left({G}\right)↔{v}\in {\mathrm{Base}}_{{S}}\right)$
20 19 biimpa ${⊢}\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\to {v}\in {\mathrm{Base}}_{{S}}$
21 20 adantr ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to {v}\in {\mathrm{Base}}_{{S}}$
22 18 difeq1d ${⊢}{\phi }\to \mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}={\mathrm{Base}}_{{S}}\setminus \left\{{v}\right\}$
23 22 eleq2d ${⊢}{\phi }\to \left({n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)↔{n}\in \left({\mathrm{Base}}_{{S}}\setminus \left\{{v}\right\}\right)\right)$
24 23 biimpd ${⊢}{\phi }\to \left({n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\to {n}\in \left({\mathrm{Base}}_{{S}}\setminus \left\{{v}\right\}\right)\right)$
25 24 adantr ${⊢}\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\to \left({n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\to {n}\in \left({\mathrm{Base}}_{{S}}\setminus \left\{{v}\right\}\right)\right)$
26 25 imp ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to {n}\in \left({\mathrm{Base}}_{{S}}\setminus \left\{{v}\right\}\right)$
27 1 cusgrexilem2 ${⊢}\left(\left({\mathrm{Base}}_{{S}}\in \mathrm{V}\wedge {v}\in {\mathrm{Base}}_{{S}}\right)\wedge {n}\in \left({\mathrm{Base}}_{{S}}\setminus \left\{{v}\right\}\right)\right)\to \exists {e}\in \mathrm{ran}\left({\mathrm{I}↾}_{{P}}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}$
28 11 21 26 27 syl21anc ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to \exists {e}\in \mathrm{ran}\left({\mathrm{I}↾}_{{P}}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}$
29 edgval ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$
30 3 fveq2i ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({S}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}↾}_{{P}}⟩\right)$
31 13 2 4 16 setsiedg ${⊢}{\phi }\to \mathrm{iEdg}\left({S}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}↾}_{{P}}⟩\right)={\mathrm{I}↾}_{{P}}$
32 30 31 syl5eq ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\right)={\mathrm{I}↾}_{{P}}$
33 32 rneqd ${⊢}{\phi }\to \mathrm{ran}\mathrm{iEdg}\left({G}\right)=\mathrm{ran}\left({\mathrm{I}↾}_{{P}}\right)$
34 29 33 syl5eq ${⊢}{\phi }\to \mathrm{Edg}\left({G}\right)=\mathrm{ran}\left({\mathrm{I}↾}_{{P}}\right)$
35 34 rexeqdv ${⊢}{\phi }\to \left(\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}↔\exists {e}\in \mathrm{ran}\left({\mathrm{I}↾}_{{P}}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}\right)$
36 35 ad2antrr ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to \left(\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}↔\exists {e}\in \mathrm{ran}\left({\mathrm{I}↾}_{{P}}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}\right)$
37 28 36 mpbird ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to \exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}$
38 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
39 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
40 38 39 nbgrel ${⊢}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)↔\left(\left({n}\in \mathrm{Vtx}\left({G}\right)\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\ne {v}\wedge \exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{n}\right\}\subseteq {e}\right)$
41 8 10 37 40 syl3anbrc ${⊢}\left(\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\right)\to {n}\in \left({G}\mathrm{NeighbVtx}{v}\right)$
42 41 ralrimiva ${⊢}\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\to \forall {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)$
43 38 uvtxel ${⊢}{v}\in \mathrm{UnivVtx}\left({G}\right)↔\left({v}\in \mathrm{Vtx}\left({G}\right)\wedge \forall {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right)$
44 6 42 43 sylanbrc ${⊢}\left({\phi }\wedge {v}\in \mathrm{Vtx}\left({G}\right)\right)\to {v}\in \mathrm{UnivVtx}\left({G}\right)$
45 44 ralrimiva ${⊢}{\phi }\to \forall {v}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)$
46 5 elexd ${⊢}{\phi }\to {G}\in \mathrm{V}$
47 38 iscplgr ${⊢}{G}\in \mathrm{V}\to \left({G}\in \mathrm{ComplGraph}↔\forall {v}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)\right)$
48 46 47 syl ${⊢}{\phi }\to \left({G}\in \mathrm{ComplGraph}↔\forall {v}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)\right)$
49 45 48 mpbird ${⊢}{\phi }\to {G}\in \mathrm{ComplGraph}$
50 iscusgr ${⊢}{G}\in \mathrm{ComplUSGraph}↔\left({G}\in \mathrm{USGraph}\wedge {G}\in \mathrm{ComplGraph}\right)$
51 5 49 50 sylanbrc ${⊢}{\phi }\to {G}\in \mathrm{ComplUSGraph}$