# 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 𝑃 = { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
structtousgr.s ( 𝜑𝑆 Struct 𝑋 )
structtousgr.g 𝐺 = ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
structtousgr.b ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
Assertion structtocusgr ( 𝜑𝐺 ∈ ComplUSGraph )

### Proof

Step Hyp Ref Expression
1 structtousgr.p 𝑃 = { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 structtousgr.s ( 𝜑𝑆 Struct 𝑋 )
3 structtousgr.g 𝐺 = ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
4 structtousgr.b ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
5 1 2 3 4 structtousgr ( 𝜑𝐺 ∈ USGraph )
6 simpr ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑣 ∈ ( Vtx ‘ 𝐺 ) )
7 eldifi ( 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) → 𝑛 ∈ ( Vtx ‘ 𝐺 ) )
8 6 7 anim12ci ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) )
9 eldifsni ( 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) → 𝑛𝑣 )
10 9 adantl ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → 𝑛𝑣 )
11 fvexd ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → ( Base ‘ 𝑆 ) ∈ V )
12 3 fveq2i ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ ) )
13 eqid ( .ef ‘ ndx ) = ( .ef ‘ ndx )
14 fvex ( Base ‘ 𝑆 ) ∈ V
15 1 cusgrexilem1 ( ( Base ‘ 𝑆 ) ∈ V → ( I ↾ 𝑃 ) ∈ V )
16 14 15 mp1i ( 𝜑 → ( I ↾ 𝑃 ) ∈ V )
17 13 2 4 16 setsvtx ( 𝜑 → ( Vtx ‘ ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ ) ) = ( Base ‘ 𝑆 ) )
18 12 17 syl5eq ( 𝜑 → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝑆 ) )
19 18 eleq2d ( 𝜑 → ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝑣 ∈ ( Base ‘ 𝑆 ) ) )
20 19 biimpa ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑣 ∈ ( Base ‘ 𝑆 ) )
21 20 adantr ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → 𝑣 ∈ ( Base ‘ 𝑆 ) )
22 18 difeq1d ( 𝜑 → ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) = ( ( Base ‘ 𝑆 ) ∖ { 𝑣 } ) )
23 22 eleq2d ( 𝜑 → ( 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ↔ 𝑛 ∈ ( ( Base ‘ 𝑆 ) ∖ { 𝑣 } ) ) )
24 23 biimpd ( 𝜑 → ( 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) → 𝑛 ∈ ( ( Base ‘ 𝑆 ) ∖ { 𝑣 } ) ) )
25 24 adantr ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) → 𝑛 ∈ ( ( Base ‘ 𝑆 ) ∖ { 𝑣 } ) ) )
26 25 imp ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → 𝑛 ∈ ( ( Base ‘ 𝑆 ) ∖ { 𝑣 } ) )
27 1 cusgrexilem2 ( ( ( ( Base ‘ 𝑆 ) ∈ V ∧ 𝑣 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑛 ∈ ( ( Base ‘ 𝑆 ) ∖ { 𝑣 } ) ) → ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )
28 11 21 26 27 syl21anc ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )
29 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
30 3 fveq2i ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ ) )
31 13 2 4 16 setsiedg ( 𝜑 → ( iEdg ‘ ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ ) ) = ( I ↾ 𝑃 ) )
32 30 31 syl5eq ( 𝜑 → ( iEdg ‘ 𝐺 ) = ( I ↾ 𝑃 ) )
33 32 rneqd ( 𝜑 → ran ( iEdg ‘ 𝐺 ) = ran ( I ↾ 𝑃 ) )
34 29 33 syl5eq ( 𝜑 → ( Edg ‘ 𝐺 ) = ran ( I ↾ 𝑃 ) )
35 34 rexeqdv ( 𝜑 → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
36 35 ad2antrr ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
37 28 36 mpbird ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )
38 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
39 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
40 38 39 nbgrel ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛𝑣 ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
41 8 10 37 40 syl3anbrc ( ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) )
42 41 ralrimiva ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) )
43 38 uvtxel ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
44 6 42 43 sylanbrc ( ( 𝜑𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
45 44 ralrimiva ( 𝜑 → ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
46 5 elexd ( 𝜑𝐺 ∈ V )
47 38 iscplgr ( 𝐺 ∈ V → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
48 46 47 syl ( 𝜑 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
49 45 48 mpbird ( 𝜑𝐺 ∈ ComplGraph )
50 iscusgr ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) )
51 5 49 50 sylanbrc ( 𝜑𝐺 ∈ ComplUSGraph )