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 )