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