Metamath Proof Explorer


Theorem cusgrexi

Description: An arbitrary set V regarded as set of vertices together with the set of pairs of elements of this set regarded as edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis usgrexi.p
|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion cusgrexi
|- ( V e. W -> <. V , ( _I |` P ) >. e. ComplUSGraph )

Proof

Step Hyp Ref Expression
1 usgrexi.p
 |-  P = { x e. ~P V | ( # ` x ) = 2 }
2 1 usgrexi
 |-  ( V e. W -> <. V , ( _I |` P ) >. e. USGraph )
3 1 cusgrexilem1
 |-  ( V e. W -> ( _I |` P ) e. _V )
4 opvtxfv
 |-  ( ( V e. W /\ ( _I |` P ) e. _V ) -> ( Vtx ` <. V , ( _I |` P ) >. ) = V )
5 4 eqcomd
 |-  ( ( V e. W /\ ( _I |` P ) e. _V ) -> V = ( Vtx ` <. V , ( _I |` P ) >. ) )
6 3 5 mpdan
 |-  ( V e. W -> V = ( Vtx ` <. V , ( _I |` P ) >. ) )
7 6 eleq2d
 |-  ( V e. W -> ( v e. V <-> v e. ( Vtx ` <. V , ( _I |` P ) >. ) ) )
8 7 biimpa
 |-  ( ( V e. W /\ v e. V ) -> v e. ( Vtx ` <. V , ( _I |` P ) >. ) )
9 eldifi
 |-  ( n e. ( V \ { v } ) -> n e. V )
10 9 adantl
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> n e. V )
11 3 4 mpdan
 |-  ( V e. W -> ( Vtx ` <. V , ( _I |` P ) >. ) = V )
12 11 eleq2d
 |-  ( V e. W -> ( n e. ( Vtx ` <. V , ( _I |` P ) >. ) <-> n e. V ) )
13 12 ad2antrr
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( n e. ( Vtx ` <. V , ( _I |` P ) >. ) <-> n e. V ) )
14 10 13 mpbird
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> n e. ( Vtx ` <. V , ( _I |` P ) >. ) )
15 simplr
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> v e. V )
16 11 eleq2d
 |-  ( V e. W -> ( v e. ( Vtx ` <. V , ( _I |` P ) >. ) <-> v e. V ) )
17 16 ad2antrr
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( v e. ( Vtx ` <. V , ( _I |` P ) >. ) <-> v e. V ) )
18 15 17 mpbird
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> v e. ( Vtx ` <. V , ( _I |` P ) >. ) )
19 14 18 jca
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( n e. ( Vtx ` <. V , ( _I |` P ) >. ) /\ v e. ( Vtx ` <. V , ( _I |` P ) >. ) ) )
20 eldifsni
 |-  ( n e. ( V \ { v } ) -> n =/= v )
21 20 adantl
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> n =/= v )
22 1 cusgrexilem2
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> E. e e. ran ( _I |` P ) { v , n } C_ e )
23 edgval
 |-  ( Edg ` <. V , ( _I |` P ) >. ) = ran ( iEdg ` <. V , ( _I |` P ) >. )
24 opiedgfv
 |-  ( ( V e. W /\ ( _I |` P ) e. _V ) -> ( iEdg ` <. V , ( _I |` P ) >. ) = ( _I |` P ) )
25 3 24 mpdan
 |-  ( V e. W -> ( iEdg ` <. V , ( _I |` P ) >. ) = ( _I |` P ) )
26 25 rneqd
 |-  ( V e. W -> ran ( iEdg ` <. V , ( _I |` P ) >. ) = ran ( _I |` P ) )
27 23 26 syl5eq
 |-  ( V e. W -> ( Edg ` <. V , ( _I |` P ) >. ) = ran ( _I |` P ) )
28 27 rexeqdv
 |-  ( V e. W -> ( E. e e. ( Edg ` <. V , ( _I |` P ) >. ) { v , n } C_ e <-> E. e e. ran ( _I |` P ) { v , n } C_ e ) )
29 28 ad2antrr
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( E. e e. ( Edg ` <. V , ( _I |` P ) >. ) { v , n } C_ e <-> E. e e. ran ( _I |` P ) { v , n } C_ e ) )
30 22 29 mpbird
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> E. e e. ( Edg ` <. V , ( _I |` P ) >. ) { v , n } C_ e )
31 eqid
 |-  ( Vtx ` <. V , ( _I |` P ) >. ) = ( Vtx ` <. V , ( _I |` P ) >. )
32 eqid
 |-  ( Edg ` <. V , ( _I |` P ) >. ) = ( Edg ` <. V , ( _I |` P ) >. )
33 31 32 nbgrel
 |-  ( n e. ( <. V , ( _I |` P ) >. NeighbVtx v ) <-> ( ( n e. ( Vtx ` <. V , ( _I |` P ) >. ) /\ v e. ( Vtx ` <. V , ( _I |` P ) >. ) ) /\ n =/= v /\ E. e e. ( Edg ` <. V , ( _I |` P ) >. ) { v , n } C_ e ) )
34 19 21 30 33 syl3anbrc
 |-  ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> n e. ( <. V , ( _I |` P ) >. NeighbVtx v ) )
35 34 ralrimiva
 |-  ( ( V e. W /\ v e. V ) -> A. n e. ( V \ { v } ) n e. ( <. V , ( _I |` P ) >. NeighbVtx v ) )
36 11 adantr
 |-  ( ( V e. W /\ v e. V ) -> ( Vtx ` <. V , ( _I |` P ) >. ) = V )
37 36 difeq1d
 |-  ( ( V e. W /\ v e. V ) -> ( ( Vtx ` <. V , ( _I |` P ) >. ) \ { v } ) = ( V \ { v } ) )
38 37 raleqdv
 |-  ( ( V e. W /\ v e. V ) -> ( A. n e. ( ( Vtx ` <. V , ( _I |` P ) >. ) \ { v } ) n e. ( <. V , ( _I |` P ) >. NeighbVtx v ) <-> A. n e. ( V \ { v } ) n e. ( <. V , ( _I |` P ) >. NeighbVtx v ) ) )
39 35 38 mpbird
 |-  ( ( V e. W /\ v e. V ) -> A. n e. ( ( Vtx ` <. V , ( _I |` P ) >. ) \ { v } ) n e. ( <. V , ( _I |` P ) >. NeighbVtx v ) )
40 31 uvtxel
 |-  ( v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) <-> ( v e. ( Vtx ` <. V , ( _I |` P ) >. ) /\ A. n e. ( ( Vtx ` <. V , ( _I |` P ) >. ) \ { v } ) n e. ( <. V , ( _I |` P ) >. NeighbVtx v ) ) )
41 8 39 40 sylanbrc
 |-  ( ( V e. W /\ v e. V ) -> v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) )
42 41 ralrimiva
 |-  ( V e. W -> A. v e. V v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) )
43 11 raleqdv
 |-  ( V e. W -> ( A. v e. ( Vtx ` <. V , ( _I |` P ) >. ) v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) <-> A. v e. V v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) ) )
44 42 43 mpbird
 |-  ( V e. W -> A. v e. ( Vtx ` <. V , ( _I |` P ) >. ) v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) )
45 opex
 |-  <. V , ( _I |` P ) >. e. _V
46 31 iscplgr
 |-  ( <. V , ( _I |` P ) >. e. _V -> ( <. V , ( _I |` P ) >. e. ComplGraph <-> A. v e. ( Vtx ` <. V , ( _I |` P ) >. ) v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) ) )
47 45 46 mp1i
 |-  ( V e. W -> ( <. V , ( _I |` P ) >. e. ComplGraph <-> A. v e. ( Vtx ` <. V , ( _I |` P ) >. ) v e. ( UnivVtx ` <. V , ( _I |` P ) >. ) ) )
48 44 47 mpbird
 |-  ( V e. W -> <. V , ( _I |` P ) >. e. ComplGraph )
49 iscusgr
 |-  ( <. V , ( _I |` P ) >. e. ComplUSGraph <-> ( <. V , ( _I |` P ) >. e. USGraph /\ <. V , ( _I |` P ) >. e. ComplGraph ) )
50 2 48 49 sylanbrc
 |-  ( V e. W -> <. V , ( _I |` P ) >. e. ComplUSGraph )