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 e. ~P ( Base ` S ) | ( # ` x ) = 2 }
structtousgr.s 
|- ( ph -> S Struct X )
structtousgr.g 
|- G = ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )
structtousgr.b 
|- ( ph -> ( Base ` ndx ) e. dom S )
Assertion structtocusgr 
|- ( ph -> G e. ComplUSGraph )

Proof

Step Hyp Ref Expression
1 structtousgr.p 
 |-  P = { x e. ~P ( Base ` S ) | ( # ` x ) = 2 }
2 structtousgr.s 
 |-  ( ph -> S Struct X )
3 structtousgr.g 
 |-  G = ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )
4 structtousgr.b 
 |-  ( ph -> ( Base ` ndx ) e. dom S )
5 1 2 3 4 structtousgr 
 |-  ( ph -> G e. USGraph )
6 simpr 
 |-  ( ( ph /\ v e. ( Vtx ` G ) ) -> v e. ( Vtx ` G ) )
7 eldifi 
 |-  ( n e. ( ( Vtx ` G ) \ { v } ) -> n e. ( Vtx ` G ) )
8 6 7 anim12ci 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> ( n e. ( Vtx ` G ) /\ v e. ( Vtx ` G ) ) )
9 eldifsni 
 |-  ( n e. ( ( Vtx ` G ) \ { v } ) -> n =/= v )
10 9 adantl 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> n =/= v )
11 fvexd 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> ( Base ` S ) e. _V )
12 3 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. ) )
13 eqid 
 |-  ( .ef ` ndx ) = ( .ef ` ndx )
14 fvex 
 |-  ( Base ` S ) e. _V
15 1 cusgrexilem1 
 |-  ( ( Base ` S ) e. _V -> ( _I |` P ) e. _V )
16 14 15 mp1i 
 |-  ( ph -> ( _I |` P ) e. _V )
17 13 2 4 16 setsvtx 
 |-  ( ph -> ( Vtx ` ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. ) ) = ( Base ` S ) )
18 12 17 eqtrid 
 |-  ( ph -> ( Vtx ` G ) = ( Base ` S ) )
19 18 eleq2d 
 |-  ( ph -> ( v e. ( Vtx ` G ) <-> v e. ( Base ` S ) ) )
20 19 biimpa 
 |-  ( ( ph /\ v e. ( Vtx ` G ) ) -> v e. ( Base ` S ) )
21 20 adantr 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> v e. ( Base ` S ) )
22 18 difeq1d 
 |-  ( ph -> ( ( Vtx ` G ) \ { v } ) = ( ( Base ` S ) \ { v } ) )
23 22 eleq2d 
 |-  ( ph -> ( n e. ( ( Vtx ` G ) \ { v } ) <-> n e. ( ( Base ` S ) \ { v } ) ) )
24 23 biimpd 
 |-  ( ph -> ( n e. ( ( Vtx ` G ) \ { v } ) -> n e. ( ( Base ` S ) \ { v } ) ) )
25 24 adantr 
 |-  ( ( ph /\ v e. ( Vtx ` G ) ) -> ( n e. ( ( Vtx ` G ) \ { v } ) -> n e. ( ( Base ` S ) \ { v } ) ) )
26 25 imp 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> n e. ( ( Base ` S ) \ { v } ) )
27 1 cusgrexilem2 
 |-  ( ( ( ( Base ` S ) e. _V /\ v e. ( Base ` S ) ) /\ n e. ( ( Base ` S ) \ { v } ) ) -> E. e e. ran ( _I |` P ) { v , n } C_ e )
28 11 21 26 27 syl21anc 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> E. e e. ran ( _I |` P ) { v , n } C_ 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 
 |-  ( ph -> ( iEdg ` ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. ) ) = ( _I |` P ) )
32 30 31 eqtrid 
 |-  ( ph -> ( iEdg ` G ) = ( _I |` P ) )
33 32 rneqd 
 |-  ( ph -> ran ( iEdg ` G ) = ran ( _I |` P ) )
34 29 33 eqtrid 
 |-  ( ph -> ( Edg ` G ) = ran ( _I |` P ) )
35 34 rexeqdv 
 |-  ( ph -> ( E. e e. ( Edg ` G ) { v , n } C_ e <-> E. e e. ran ( _I |` P ) { v , n } C_ e ) )
36 35 ad2antrr 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> ( E. e e. ( Edg ` G ) { v , n } C_ e <-> E. e e. ran ( _I |` P ) { v , n } C_ e ) )
37 28 36 mpbird 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> E. e e. ( Edg ` G ) { v , n } C_ e )
38 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
39 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
40 38 39 nbgrel 
 |-  ( n e. ( G NeighbVtx v ) <-> ( ( n e. ( Vtx ` G ) /\ v e. ( Vtx ` G ) ) /\ n =/= v /\ E. e e. ( Edg ` G ) { v , n } C_ e ) )
41 8 10 37 40 syl3anbrc 
 |-  ( ( ( ph /\ v e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { v } ) ) -> n e. ( G NeighbVtx v ) )
42 41 ralrimiva 
 |-  ( ( ph /\ v e. ( Vtx ` G ) ) -> A. n e. ( ( Vtx ` G ) \ { v } ) n e. ( G NeighbVtx v ) )
43 38 uvtxel 
 |-  ( v e. ( UnivVtx ` G ) <-> ( v e. ( Vtx ` G ) /\ A. n e. ( ( Vtx ` G ) \ { v } ) n e. ( G NeighbVtx v ) ) )
44 6 42 43 sylanbrc 
 |-  ( ( ph /\ v e. ( Vtx ` G ) ) -> v e. ( UnivVtx ` G ) )
45 44 ralrimiva 
 |-  ( ph -> A. v e. ( Vtx ` G ) v e. ( UnivVtx ` G ) )
46 5 elexd 
 |-  ( ph -> G e. _V )
47 38 iscplgr 
 |-  ( G e. _V -> ( G e. ComplGraph <-> A. v e. ( Vtx ` G ) v e. ( UnivVtx ` G ) ) )
48 46 47 syl 
 |-  ( ph -> ( G e. ComplGraph <-> A. v e. ( Vtx ` G ) v e. ( UnivVtx ` G ) ) )
49 45 48 mpbird 
 |-  ( ph -> G e. ComplGraph )
50 iscusgr 
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
51 5 49 50 sylanbrc 
 |-  ( ph -> G e. ComplUSGraph )