Metamath Proof Explorer


Theorem cusgredg

Description: In a complete simple graph, the edges are all the pairs of different vertices. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 1-Nov-2020)

Ref Expression
Hypotheses iscusgrvtx.v
|- V = ( Vtx ` G )
iscusgredg.v
|- E = ( Edg ` G )
Assertion cusgredg
|- ( G e. ComplUSGraph -> E = { x e. ~P V | ( # ` x ) = 2 } )

Proof

Step Hyp Ref Expression
1 iscusgrvtx.v
 |-  V = ( Vtx ` G )
2 iscusgredg.v
 |-  E = ( Edg ` G )
3 1 2 iscusgredg
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ A. v e. V A. n e. ( V \ { v } ) { n , v } e. E ) )
4 usgredgss
 |-  ( G e. USGraph -> ( Edg ` G ) C_ { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
5 1 pweqi
 |-  ~P V = ~P ( Vtx ` G )
6 5 rabeqi
 |-  { x e. ~P V | ( # ` x ) = 2 } = { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 }
7 4 2 6 3sstr4g
 |-  ( G e. USGraph -> E C_ { x e. ~P V | ( # ` x ) = 2 } )
8 7 adantr
 |-  ( ( G e. USGraph /\ A. v e. V A. n e. ( V \ { v } ) { n , v } e. E ) -> E C_ { x e. ~P V | ( # ` x ) = 2 } )
9 elss2prb
 |-  ( p e. { x e. ~P V | ( # ` x ) = 2 } <-> E. y e. V E. z e. V ( y =/= z /\ p = { y , z } ) )
10 sneq
 |-  ( v = y -> { v } = { y } )
11 10 difeq2d
 |-  ( v = y -> ( V \ { v } ) = ( V \ { y } ) )
12 preq2
 |-  ( v = y -> { n , v } = { n , y } )
13 12 eleq1d
 |-  ( v = y -> ( { n , v } e. E <-> { n , y } e. E ) )
14 11 13 raleqbidv
 |-  ( v = y -> ( A. n e. ( V \ { v } ) { n , v } e. E <-> A. n e. ( V \ { y } ) { n , y } e. E ) )
15 14 rspcv
 |-  ( y e. V -> ( A. v e. V A. n e. ( V \ { v } ) { n , v } e. E -> A. n e. ( V \ { y } ) { n , y } e. E ) )
16 15 adantr
 |-  ( ( y e. V /\ z e. V ) -> ( A. v e. V A. n e. ( V \ { v } ) { n , v } e. E -> A. n e. ( V \ { y } ) { n , y } e. E ) )
17 16 adantr
 |-  ( ( ( y e. V /\ z e. V ) /\ ( y =/= z /\ p = { y , z } ) ) -> ( A. v e. V A. n e. ( V \ { v } ) { n , v } e. E -> A. n e. ( V \ { y } ) { n , y } e. E ) )
18 simpr
 |-  ( ( y e. V /\ z e. V ) -> z e. V )
19 necom
 |-  ( y =/= z <-> z =/= y )
20 19 biimpi
 |-  ( y =/= z -> z =/= y )
21 20 adantr
 |-  ( ( y =/= z /\ p = { y , z } ) -> z =/= y )
22 18 21 anim12i
 |-  ( ( ( y e. V /\ z e. V ) /\ ( y =/= z /\ p = { y , z } ) ) -> ( z e. V /\ z =/= y ) )
23 eldifsn
 |-  ( z e. ( V \ { y } ) <-> ( z e. V /\ z =/= y ) )
24 22 23 sylibr
 |-  ( ( ( y e. V /\ z e. V ) /\ ( y =/= z /\ p = { y , z } ) ) -> z e. ( V \ { y } ) )
25 preq1
 |-  ( n = z -> { n , y } = { z , y } )
26 25 eleq1d
 |-  ( n = z -> ( { n , y } e. E <-> { z , y } e. E ) )
27 26 rspcv
 |-  ( z e. ( V \ { y } ) -> ( A. n e. ( V \ { y } ) { n , y } e. E -> { z , y } e. E ) )
28 24 27 syl
 |-  ( ( ( y e. V /\ z e. V ) /\ ( y =/= z /\ p = { y , z } ) ) -> ( A. n e. ( V \ { y } ) { n , y } e. E -> { z , y } e. E ) )
29 id
 |-  ( p = { y , z } -> p = { y , z } )
30 prcom
 |-  { y , z } = { z , y }
31 29 30 eqtr2di
 |-  ( p = { y , z } -> { z , y } = p )
32 31 eleq1d
 |-  ( p = { y , z } -> ( { z , y } e. E <-> p e. E ) )
33 32 biimpd
 |-  ( p = { y , z } -> ( { z , y } e. E -> p e. E ) )
34 33 a1d
 |-  ( p = { y , z } -> ( G e. USGraph -> ( { z , y } e. E -> p e. E ) ) )
35 34 ad2antll
 |-  ( ( ( y e. V /\ z e. V ) /\ ( y =/= z /\ p = { y , z } ) ) -> ( G e. USGraph -> ( { z , y } e. E -> p e. E ) ) )
36 35 com23
 |-  ( ( ( y e. V /\ z e. V ) /\ ( y =/= z /\ p = { y , z } ) ) -> ( { z , y } e. E -> ( G e. USGraph -> p e. E ) ) )
37 17 28 36 3syld
 |-  ( ( ( y e. V /\ z e. V ) /\ ( y =/= z /\ p = { y , z } ) ) -> ( A. v e. V A. n e. ( V \ { v } ) { n , v } e. E -> ( G e. USGraph -> p e. E ) ) )
38 37 ex
 |-  ( ( y e. V /\ z e. V ) -> ( ( y =/= z /\ p = { y , z } ) -> ( A. v e. V A. n e. ( V \ { v } ) { n , v } e. E -> ( G e. USGraph -> p e. E ) ) ) )
39 38 rexlimivv
 |-  ( E. y e. V E. z e. V ( y =/= z /\ p = { y , z } ) -> ( A. v e. V A. n e. ( V \ { v } ) { n , v } e. E -> ( G e. USGraph -> p e. E ) ) )
40 39 com13
 |-  ( G e. USGraph -> ( A. v e. V A. n e. ( V \ { v } ) { n , v } e. E -> ( E. y e. V E. z e. V ( y =/= z /\ p = { y , z } ) -> p e. E ) ) )
41 40 imp
 |-  ( ( G e. USGraph /\ A. v e. V A. n e. ( V \ { v } ) { n , v } e. E ) -> ( E. y e. V E. z e. V ( y =/= z /\ p = { y , z } ) -> p e. E ) )
42 9 41 syl5bi
 |-  ( ( G e. USGraph /\ A. v e. V A. n e. ( V \ { v } ) { n , v } e. E ) -> ( p e. { x e. ~P V | ( # ` x ) = 2 } -> p e. E ) )
43 42 ssrdv
 |-  ( ( G e. USGraph /\ A. v e. V A. n e. ( V \ { v } ) { n , v } e. E ) -> { x e. ~P V | ( # ` x ) = 2 } C_ E )
44 8 43 eqssd
 |-  ( ( G e. USGraph /\ A. v e. V A. n e. ( V \ { v } ) { n , v } e. E ) -> E = { x e. ~P V | ( # ` x ) = 2 } )
45 3 44 sylbi
 |-  ( G e. ComplUSGraph -> E = { x e. ~P V | ( # ` x ) = 2 } )