Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdginducedm1.v |
|- V = ( Vtx ` G ) |
2 |
|
vtxdginducedm1.e |
|- E = ( iEdg ` G ) |
3 |
|
vtxdginducedm1.k |
|- K = ( V \ { N } ) |
4 |
|
vtxdginducedm1.i |
|- I = { i e. dom E | N e/ ( E ` i ) } |
5 |
|
vtxdginducedm1.p |
|- P = ( E |` I ) |
6 |
|
vtxdginducedm1.s |
|- S = <. K , P >. |
7 |
|
vtxdginducedm1.j |
|- J = { i e. dom E | N e. ( E ` i ) } |
8 |
|
fveq2 |
|- ( i = k -> ( E ` i ) = ( E ` k ) ) |
9 |
8
|
eleq2d |
|- ( i = k -> ( N e. ( E ` i ) <-> N e. ( E ` k ) ) ) |
10 |
9 7
|
elrab2 |
|- ( k e. J <-> ( k e. dom E /\ N e. ( E ` k ) ) ) |
11 |
|
eldifsn |
|- ( W e. ( V \ { N } ) <-> ( W e. V /\ W =/= N ) ) |
12 |
|
df-ne |
|- ( W =/= N <-> -. W = N ) |
13 |
|
eleq2 |
|- ( ( E ` k ) = { W } -> ( N e. ( E ` k ) <-> N e. { W } ) ) |
14 |
|
elsni |
|- ( N e. { W } -> N = W ) |
15 |
14
|
eqcomd |
|- ( N e. { W } -> W = N ) |
16 |
13 15
|
syl6bi |
|- ( ( E ` k ) = { W } -> ( N e. ( E ` k ) -> W = N ) ) |
17 |
16
|
com12 |
|- ( N e. ( E ` k ) -> ( ( E ` k ) = { W } -> W = N ) ) |
18 |
17
|
con3rr3 |
|- ( -. W = N -> ( N e. ( E ` k ) -> -. ( E ` k ) = { W } ) ) |
19 |
12 18
|
sylbi |
|- ( W =/= N -> ( N e. ( E ` k ) -> -. ( E ` k ) = { W } ) ) |
20 |
11 19
|
simplbiim |
|- ( W e. ( V \ { N } ) -> ( N e. ( E ` k ) -> -. ( E ` k ) = { W } ) ) |
21 |
20
|
com12 |
|- ( N e. ( E ` k ) -> ( W e. ( V \ { N } ) -> -. ( E ` k ) = { W } ) ) |
22 |
10 21
|
simplbiim |
|- ( k e. J -> ( W e. ( V \ { N } ) -> -. ( E ` k ) = { W } ) ) |
23 |
22
|
impcom |
|- ( ( W e. ( V \ { N } ) /\ k e. J ) -> -. ( E ` k ) = { W } ) |
24 |
23
|
ralrimiva |
|- ( W e. ( V \ { N } ) -> A. k e. J -. ( E ` k ) = { W } ) |
25 |
|
rabeq0 |
|- ( { k e. J | ( E ` k ) = { W } } = (/) <-> A. k e. J -. ( E ` k ) = { W } ) |
26 |
24 25
|
sylibr |
|- ( W e. ( V \ { N } ) -> { k e. J | ( E ` k ) = { W } } = (/) ) |
27 |
2
|
fvexi |
|- E e. _V |
28 |
27
|
dmex |
|- dom E e. _V |
29 |
7 28
|
rab2ex |
|- { k e. J | ( E ` k ) = { W } } e. _V |
30 |
|
hasheq0 |
|- ( { k e. J | ( E ` k ) = { W } } e. _V -> ( ( # ` { k e. J | ( E ` k ) = { W } } ) = 0 <-> { k e. J | ( E ` k ) = { W } } = (/) ) ) |
31 |
29 30
|
ax-mp |
|- ( ( # ` { k e. J | ( E ` k ) = { W } } ) = 0 <-> { k e. J | ( E ` k ) = { W } } = (/) ) |
32 |
26 31
|
sylibr |
|- ( W e. ( V \ { N } ) -> ( # ` { k e. J | ( E ` k ) = { W } } ) = 0 ) |