This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid 
 |-  ( ( 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 } )