Step |
Hyp |
Ref |
Expression |
1 |
|
frgrwopreg.v |
|- V = ( Vtx ` G ) |
2 |
|
frgrwopreg.d |
|- D = ( VtxDeg ` G ) |
3 |
|
frgrwopreg.a |
|- A = { x e. V | ( D ` x ) = K } |
4 |
|
frgrwopreg.b |
|- B = ( V \ A ) |
5 |
|
n0 |
|- ( A =/= (/) <-> E. x x e. A ) |
6 |
3
|
rabeq2i |
|- ( x e. A <-> ( x e. V /\ ( D ` x ) = K ) ) |
7 |
1
|
vdgfrgrgt2 |
|- ( ( G e. FriendGraph /\ x e. V ) -> ( 1 < ( # ` V ) -> 2 <_ ( ( VtxDeg ` G ) ` x ) ) ) |
8 |
7
|
imp |
|- ( ( ( G e. FriendGraph /\ x e. V ) /\ 1 < ( # ` V ) ) -> 2 <_ ( ( VtxDeg ` G ) ` x ) ) |
9 |
|
breq2 |
|- ( K = ( D ` x ) -> ( 2 <_ K <-> 2 <_ ( D ` x ) ) ) |
10 |
2
|
fveq1i |
|- ( D ` x ) = ( ( VtxDeg ` G ) ` x ) |
11 |
10
|
breq2i |
|- ( 2 <_ ( D ` x ) <-> 2 <_ ( ( VtxDeg ` G ) ` x ) ) |
12 |
9 11
|
syl6bb |
|- ( K = ( D ` x ) -> ( 2 <_ K <-> 2 <_ ( ( VtxDeg ` G ) ` x ) ) ) |
13 |
12
|
eqcoms |
|- ( ( D ` x ) = K -> ( 2 <_ K <-> 2 <_ ( ( VtxDeg ` G ) ` x ) ) ) |
14 |
8 13
|
syl5ibrcom |
|- ( ( ( G e. FriendGraph /\ x e. V ) /\ 1 < ( # ` V ) ) -> ( ( D ` x ) = K -> 2 <_ K ) ) |
15 |
14
|
exp31 |
|- ( G e. FriendGraph -> ( x e. V -> ( 1 < ( # ` V ) -> ( ( D ` x ) = K -> 2 <_ K ) ) ) ) |
16 |
15
|
com14 |
|- ( ( D ` x ) = K -> ( x e. V -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) ) ) |
17 |
16
|
impcom |
|- ( ( x e. V /\ ( D ` x ) = K ) -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) ) |
18 |
6 17
|
sylbi |
|- ( x e. A -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) ) |
19 |
18
|
exlimiv |
|- ( E. x x e. A -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) ) |
20 |
5 19
|
sylbi |
|- ( A =/= (/) -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> 2 <_ K ) ) ) |
21 |
20
|
3imp31 |
|- ( ( G e. FriendGraph /\ 1 < ( # ` V ) /\ A =/= (/) ) -> 2 <_ K ) |