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

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 biimtrdi 
 |-  ( ( 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 )