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