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 eqtrid ⊢ ( 𝜑 → ( 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 eqtrid ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ( I ↾ 𝑃 ) )
33 32 rneqd ⊢ ( 𝜑 → ran ( iEdg ‘ 𝐺 ) = ran ( I ↾ 𝑃 ) )
34 29 33 eqtrid ⊢ ( 𝜑 → ( 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 )