Metamath Proof Explorer


Theorem vtxdginducedm1lem4

Description: Lemma 4 for vtxdginducedm1 . (Contributed by AV, 17-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v
|- V = ( Vtx ` G )
vtxdginducedm1.e
|- E = ( iEdg ` G )
vtxdginducedm1.k
|- K = ( V \ { N } )
vtxdginducedm1.i
|- I = { i e. dom E | N e/ ( E ` i ) }
vtxdginducedm1.p
|- P = ( E |` I )
vtxdginducedm1.s
|- S = <. K , P >.
vtxdginducedm1.j
|- J = { i e. dom E | N e. ( E ` i ) }
Assertion vtxdginducedm1lem4
|- ( W e. ( V \ { N } ) -> ( # ` { k e. J | ( E ` k ) = { W } } ) = 0 )

Proof

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 )