# 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 = x ∈ 𝒫 Base S | x = 2$
structtousgr.s $⊢ φ → S Struct X$
structtousgr.g $⊢ G = S sSet ef ⁡ ndx I ↾ P$
structtousgr.b $⊢ φ → Base ndx ∈ dom ⁡ S$
Assertion structtocusgr $⊢ φ → G ∈ ComplUSGraph$

### Proof

Step Hyp Ref Expression
1 structtousgr.p $⊢ P = x ∈ 𝒫 Base S | x = 2$
2 structtousgr.s $⊢ φ → S Struct X$
3 structtousgr.g $⊢ G = S sSet ef ⁡ ndx I ↾ P$
4 structtousgr.b $⊢ φ → Base ndx ∈ dom ⁡ S$
5 1 2 3 4 structtousgr $⊢ φ → G ∈ USGraph$
6 simpr $⊢ φ ∧ v ∈ Vtx ⁡ G → v ∈ Vtx ⁡ G$
7 eldifi $⊢ n ∈ Vtx ⁡ G ∖ v → n ∈ Vtx ⁡ G$
8 6 7 anim12ci $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → n ∈ Vtx ⁡ G ∧ v ∈ Vtx ⁡ G$
9 eldifsni $⊢ n ∈ Vtx ⁡ G ∖ v → n ≠ v$
10 9 adantl $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → n ≠ v$
11 fvexd $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → Base S ∈ V$
12 3 fveq2i $⊢ Vtx ⁡ G = Vtx ⁡ S sSet ef ⁡ ndx I ↾ P$
13 eqid $⊢ ef ⁡ ndx = ef ⁡ ndx$
14 fvex $⊢ Base S ∈ V$
15 1 cusgrexilem1 $⊢ Base S ∈ V → I ↾ P ∈ V$
16 14 15 mp1i $⊢ φ → I ↾ P ∈ V$
17 13 2 4 16 setsvtx $⊢ φ → Vtx ⁡ S sSet ef ⁡ ndx I ↾ P = Base S$
18 12 17 syl5eq $⊢ φ → Vtx ⁡ G = Base S$
19 18 eleq2d $⊢ φ → v ∈ Vtx ⁡ G ↔ v ∈ Base S$
20 19 biimpa $⊢ φ ∧ v ∈ Vtx ⁡ G → v ∈ Base S$
21 20 adantr $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → v ∈ Base S$
22 18 difeq1d $⊢ φ → Vtx ⁡ G ∖ v = Base S ∖ v$
23 22 eleq2d $⊢ φ → n ∈ Vtx ⁡ G ∖ v ↔ n ∈ Base S ∖ v$
24 23 biimpd $⊢ φ → n ∈ Vtx ⁡ G ∖ v → n ∈ Base S ∖ v$
25 24 adantr $⊢ φ ∧ v ∈ Vtx ⁡ G → n ∈ Vtx ⁡ G ∖ v → n ∈ Base S ∖ v$
26 25 imp $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → n ∈ Base S ∖ v$
27 1 cusgrexilem2 $⊢ Base S ∈ V ∧ v ∈ Base S ∧ n ∈ Base S ∖ v → ∃ e ∈ ran ⁡ I ↾ P v n ⊆ e$
28 11 21 26 27 syl21anc $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → ∃ e ∈ ran ⁡ I ↾ P v n ⊆ e$
29 edgval $⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G$
30 3 fveq2i $⊢ iEdg ⁡ G = iEdg ⁡ S sSet ef ⁡ ndx I ↾ P$
31 13 2 4 16 setsiedg $⊢ φ → iEdg ⁡ S sSet ef ⁡ ndx I ↾ P = I ↾ P$
32 30 31 syl5eq $⊢ φ → iEdg ⁡ G = I ↾ P$
33 32 rneqd $⊢ φ → ran ⁡ iEdg ⁡ G = ran ⁡ I ↾ P$
34 29 33 syl5eq $⊢ φ → Edg ⁡ G = ran ⁡ I ↾ P$
35 34 rexeqdv $⊢ φ → ∃ e ∈ Edg ⁡ G v n ⊆ e ↔ ∃ e ∈ ran ⁡ I ↾ P v n ⊆ e$
36 35 ad2antrr $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → ∃ e ∈ Edg ⁡ G v n ⊆ e ↔ ∃ e ∈ ran ⁡ I ↾ P v n ⊆ e$
37 28 36 mpbird $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → ∃ e ∈ Edg ⁡ G v n ⊆ e$
38 eqid $⊢ Vtx ⁡ G = Vtx ⁡ G$
39 eqid $⊢ Edg ⁡ G = Edg ⁡ G$
40 38 39 nbgrel $⊢ n ∈ G NeighbVtx v ↔ n ∈ Vtx ⁡ G ∧ v ∈ Vtx ⁡ G ∧ n ≠ v ∧ ∃ e ∈ Edg ⁡ G v n ⊆ e$
41 8 10 37 40 syl3anbrc $⊢ φ ∧ v ∈ Vtx ⁡ G ∧ n ∈ Vtx ⁡ G ∖ v → n ∈ G NeighbVtx v$
42 41 ralrimiva $⊢ φ ∧ v ∈ Vtx ⁡ G → ∀ n ∈ Vtx ⁡ G ∖ v n ∈ G NeighbVtx v$
43 38 uvtxel $⊢ v ∈ UnivVtx ⁡ G ↔ v ∈ Vtx ⁡ G ∧ ∀ n ∈ Vtx ⁡ G ∖ v n ∈ G NeighbVtx v$
44 6 42 43 sylanbrc $⊢ φ ∧ v ∈ Vtx ⁡ G → v ∈ UnivVtx ⁡ G$
45 44 ralrimiva $⊢ φ → ∀ v ∈ Vtx ⁡ G v ∈ UnivVtx ⁡ G$
46 5 elexd $⊢ φ → G ∈ V$
47 38 iscplgr $⊢ G ∈ V → G ∈ ComplGraph ↔ ∀ v ∈ Vtx ⁡ G v ∈ UnivVtx ⁡ G$
48 46 47 syl $⊢ φ → G ∈ ComplGraph ↔ ∀ v ∈ Vtx ⁡ G v ∈ UnivVtx ⁡ G$
49 45 48 mpbird $⊢ φ → G ∈ ComplGraph$
50 iscusgr $⊢ G ∈ ComplUSGraph ↔ G ∈ USGraph ∧ G ∈ ComplGraph$
51 5 49 50 sylanbrc $⊢ φ → G ∈ ComplUSGraph$