Metamath Proof Explorer

Theorem numedglnl

Description: The number of edges incident with a vertex N is the number of edges joining N with other vertices and the number of loops on N in a pseudograph of finite size. (Contributed by AV, 19-Dec-2021)

Ref Expression
Hypotheses edglnl.v 
|- V = ( Vtx ` G )
edglnl.e 
|- E = ( iEdg ` G )
Assertion numedglnl 
|- ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` { i e. dom E | N e. ( E ` i ) } ) )

Proof

Step Hyp Ref Expression
1 edglnl.v 
 |-  V = ( Vtx ` G )
2 edglnl.e 
 |-  E = ( iEdg ` G )
3 diffi 
 |-  ( V e. Fin -> ( V \ { N } ) e. Fin )
4 3 adantr 
 |-  ( ( V e. Fin /\ E e. Fin ) -> ( V \ { N } ) e. Fin )
5 4 3ad2ant2 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( V \ { N } ) e. Fin )
6 dmfi 
 |-  ( E e. Fin -> dom E e. Fin )
7 rabfi 
 |-  ( dom E e. Fin -> { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
8 6 7 syl 
 |-  ( E e. Fin -> { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
9 8 adantl 
 |-  ( ( V e. Fin /\ E e. Fin ) -> { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
10 9 3ad2ant2 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
11 10 adantr 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ v e. ( V \ { N } ) ) -> { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
12 notnotb 
 |-  ( N e. ( E ` i ) <-> -. -. N e. ( E ` i ) )
13 notnotb 
 |-  ( v e. ( E ` i ) <-> -. -. v e. ( E ` i ) )
14 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
15 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun E )
16 14 15 syl 
 |-  ( G e. UPGraph -> Fun E )
17 2 iedgedg 
 |-  ( ( Fun E /\ i e. dom E ) -> ( E ` i ) e. ( Edg ` G ) )
18 16 17 sylan 
 |-  ( ( G e. UPGraph /\ i e. dom E ) -> ( E ` i ) e. ( Edg ` G ) )
19 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
20 1 19 upgredg 
 |-  ( ( G e. UPGraph /\ ( E ` i ) e. ( Edg ` G ) ) -> E. m e. V E. n e. V ( E ` i ) = { m , n } )
21 18 20 syldan 
 |-  ( ( G e. UPGraph /\ i e. dom E ) -> E. m e. V E. n e. V ( E ` i ) = { m , n } )
22 21 ex 
 |-  ( G e. UPGraph -> ( i e. dom E -> E. m e. V E. n e. V ( E ` i ) = { m , n } ) )
23 22 3ad2ant1 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( i e. dom E -> E. m e. V E. n e. V ( E ` i ) = { m , n } ) )
24 23 adantr 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) -> ( i e. dom E -> E. m e. V E. n e. V ( E ` i ) = { m , n } ) )
25 24 adantr 
 |-  ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) -> ( i e. dom E -> E. m e. V E. n e. V ( E ` i ) = { m , n } ) )
26 25 imp 
 |-  ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) -> E. m e. V E. n e. V ( E ` i ) = { m , n } )
27 eldifsni 
 |-  ( v e. ( V \ { N } ) -> v =/= N )
28 eldifsni 
 |-  ( w e. ( V \ { N } ) -> w =/= N )
29 3elpr2eq 
 |-  ( ( ( N e. { m , n } /\ v e. { m , n } /\ w e. { m , n } ) /\ ( v =/= N /\ w =/= N ) ) -> v = w )
30 29 expcom 
 |-  ( ( v =/= N /\ w =/= N ) -> ( ( N e. { m , n } /\ v e. { m , n } /\ w e. { m , n } ) -> v = w ) )
31 30 3expd 
 |-  ( ( v =/= N /\ w =/= N ) -> ( N e. { m , n } -> ( v e. { m , n } -> ( w e. { m , n } -> v = w ) ) ) )
32 31 com23 
 |-  ( ( v =/= N /\ w =/= N ) -> ( v e. { m , n } -> ( N e. { m , n } -> ( w e. { m , n } -> v = w ) ) ) )
33 32 3imp 
 |-  ( ( ( v =/= N /\ w =/= N ) /\ v e. { m , n } /\ N e. { m , n } ) -> ( w e. { m , n } -> v = w ) )
34 33 con3d 
 |-  ( ( ( v =/= N /\ w =/= N ) /\ v e. { m , n } /\ N e. { m , n } ) -> ( -. v = w -> -. w e. { m , n } ) )
35 34 3exp 
 |-  ( ( v =/= N /\ w =/= N ) -> ( v e. { m , n } -> ( N e. { m , n } -> ( -. v = w -> -. w e. { m , n } ) ) ) )
36 35 com24 
 |-  ( ( v =/= N /\ w =/= N ) -> ( -. v = w -> ( N e. { m , n } -> ( v e. { m , n } -> -. w e. { m , n } ) ) ) )
37 36 imp 
 |-  ( ( ( v =/= N /\ w =/= N ) /\ -. v = w ) -> ( N e. { m , n } -> ( v e. { m , n } -> -. w e. { m , n } ) ) )
38 eleq2 
 |-  ( ( E ` i ) = { m , n } -> ( N e. ( E ` i ) <-> N e. { m , n } ) )
39 eleq2 
 |-  ( ( E ` i ) = { m , n } -> ( v e. ( E ` i ) <-> v e. { m , n } ) )
40 eleq2 
 |-  ( ( E ` i ) = { m , n } -> ( w e. ( E ` i ) <-> w e. { m , n } ) )
41 40 notbid 
 |-  ( ( E ` i ) = { m , n } -> ( -. w e. ( E ` i ) <-> -. w e. { m , n } ) )
42 39 41 imbi12d 
 |-  ( ( E ` i ) = { m , n } -> ( ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) <-> ( v e. { m , n } -> -. w e. { m , n } ) ) )
43 38 42 imbi12d 
 |-  ( ( E ` i ) = { m , n } -> ( ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) <-> ( N e. { m , n } -> ( v e. { m , n } -> -. w e. { m , n } ) ) ) )
44 37 43 syl5ibrcom 
 |-  ( ( ( v =/= N /\ w =/= N ) /\ -. v = w ) -> ( ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) )
45 44 adantr 
 |-  ( ( ( ( v =/= N /\ w =/= N ) /\ -. v = w ) /\ ( m e. V /\ n e. V ) ) -> ( ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) )
46 45 rexlimdvva 
 |-  ( ( ( v =/= N /\ w =/= N ) /\ -. v = w ) -> ( E. m e. V E. n e. V ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) )
47 46 ex 
 |-  ( ( v =/= N /\ w =/= N ) -> ( -. v = w -> ( E. m e. V E. n e. V ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) ) )
48 27 28 47 syl2an 
 |-  ( ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) -> ( -. v = w -> ( E. m e. V E. n e. V ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) ) )
49 48 adantl 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) -> ( -. v = w -> ( E. m e. V E. n e. V ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) ) )
50 49 imp 
 |-  ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) -> ( E. m e. V E. n e. V ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) )
51 50 adantr 
 |-  ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) -> ( E. m e. V E. n e. V ( E ` i ) = { m , n } -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) ) )
52 26 51 mpd 
 |-  ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) -> ( N e. ( E ` i ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) ) )
53 52 imp 
 |-  ( ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) /\ N e. ( E ` i ) ) -> ( v e. ( E ` i ) -> -. w e. ( E ` i ) ) )
54 13 53 biimtrrid 
 |-  ( ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) /\ N e. ( E ` i ) ) -> ( -. -. v e. ( E ` i ) -> -. w e. ( E ` i ) ) )
55 54 orrd 
 |-  ( ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) /\ N e. ( E ` i ) ) -> ( -. v e. ( E ` i ) \/ -. w e. ( E ` i ) ) )
56 55 ex 
 |-  ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) -> ( N e. ( E ` i ) -> ( -. v e. ( E ` i ) \/ -. w e. ( E ` i ) ) ) )
57 12 56 biimtrrid 
 |-  ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) -> ( -. -. N e. ( E ` i ) -> ( -. v e. ( E ` i ) \/ -. w e. ( E ` i ) ) ) )
58 57 orrd 
 |-  ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) -> ( -. N e. ( E ` i ) \/ ( -. v e. ( E ` i ) \/ -. w e. ( E ` i ) ) ) )
59 anandi 
 |-  ( ( N e. ( E ` i ) /\ ( v e. ( E ` i ) /\ w e. ( E ` i ) ) ) <-> ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
60 59 bicomi 
 |-  ( ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) <-> ( N e. ( E ` i ) /\ ( v e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
61 60 notbii 
 |-  ( -. ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) <-> -. ( N e. ( E ` i ) /\ ( v e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
62 ianor 
 |-  ( -. ( N e. ( E ` i ) /\ ( v e. ( E ` i ) /\ w e. ( E ` i ) ) ) <-> ( -. N e. ( E ` i ) \/ -. ( v e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
63 ianor 
 |-  ( -. ( v e. ( E ` i ) /\ w e. ( E ` i ) ) <-> ( -. v e. ( E ` i ) \/ -. w e. ( E ` i ) ) )
64 63 orbi2i 
 |-  ( ( -. N e. ( E ` i ) \/ -. ( v e. ( E ` i ) /\ w e. ( E ` i ) ) ) <-> ( -. N e. ( E ` i ) \/ ( -. v e. ( E ` i ) \/ -. w e. ( E ` i ) ) ) )
65 61 62 64 3bitri 
 |-  ( -. ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) <-> ( -. N e. ( E ` i ) \/ ( -. v e. ( E ` i ) \/ -. w e. ( E ` i ) ) ) )
66 58 65 sylibr 
 |-  ( ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) /\ i e. dom E ) -> -. ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
67 66 ralrimiva 
 |-  ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) -> A. i e. dom E -. ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
68 inrab 
 |-  ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = { i e. dom E | ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) }
69 68 eqeq1i 
 |-  ( ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = (/) <-> { i e. dom E | ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) } = (/) )
70 rabeq0 
 |-  ( { i e. dom E | ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) } = (/) <-> A. i e. dom E -. ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
71 69 70 bitri 
 |-  ( ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = (/) <-> A. i e. dom E -. ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) /\ ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
72 67 71 sylibr 
 |-  ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) /\ -. v = w ) -> ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = (/) )
73 72 ex 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) -> ( -. v = w -> ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = (/) ) )
74 73 orrd 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( v e. ( V \ { N } ) /\ w e. ( V \ { N } ) ) ) -> ( v = w \/ ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = (/) ) )
75 74 ralrimivva 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> A. v e. ( V \ { N } ) A. w e. ( V \ { N } ) ( v = w \/ ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = (/) ) )
76 eleq1w 
 |-  ( v = w -> ( v e. ( E ` i ) <-> w e. ( E ` i ) ) )
77 76 anbi2d 
 |-  ( v = w -> ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) <-> ( N e. ( E ` i ) /\ w e. ( E ` i ) ) ) )
78 77 rabbidv 
 |-  ( v = w -> { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } = { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } )
79 78 disjor 
 |-  ( Disj_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> A. v e. ( V \ { N } ) A. w e. ( V \ { N } ) ( v = w \/ ( { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( N e. ( E ` i ) /\ w e. ( E ` i ) ) } ) = (/) ) )
80 75 79 sylibr 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> Disj_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
81 5 11 80 hashiun 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( # ` U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) = sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) )
82 81 eqcomd 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) = ( # ` U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) )
83 82 oveq1d 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( ( # ` U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) )
84 11 ralrimiva 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> A. v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
85 iunfi 
 |-  ( ( ( V \ { N } ) e. Fin /\ A. v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin ) -> U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
86 5 84 85 syl2anc 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin )
87 rabfi 
 |-  ( dom E e. Fin -> { i e. dom E | ( E ` i ) = { N } } e. Fin )
88 6 87 syl 
 |-  ( E e. Fin -> { i e. dom E | ( E ` i ) = { N } } e. Fin )
89 88 adantl 
 |-  ( ( V e. Fin /\ E e. Fin ) -> { i e. dom E | ( E ` i ) = { N } } e. Fin )
90 89 3ad2ant2 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> { i e. dom E | ( E ` i ) = { N } } e. Fin )
91 fveqeq2 
 |-  ( i = j -> ( ( E ` i ) = { N } <-> ( E ` j ) = { N } ) )
92 91 elrab 
 |-  ( j e. { i e. dom E | ( E ` i ) = { N } } <-> ( j e. dom E /\ ( E ` j ) = { N } ) )
93 eldifn 
 |-  ( v e. ( V \ { N } ) -> -. v e. { N } )
94 eleq2 
 |-  ( ( E ` j ) = { N } -> ( v e. ( E ` j ) <-> v e. { N } ) )
95 94 notbid 
 |-  ( ( E ` j ) = { N } -> ( -. v e. ( E ` j ) <-> -. v e. { N } ) )
96 93 95 imbitrrid 
 |-  ( ( E ` j ) = { N } -> ( v e. ( V \ { N } ) -> -. v e. ( E ` j ) ) )
97 96 adantl 
 |-  ( ( j e. dom E /\ ( E ` j ) = { N } ) -> ( v e. ( V \ { N } ) -> -. v e. ( E ` j ) ) )
98 97 adantl 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( j e. dom E /\ ( E ` j ) = { N } ) ) -> ( v e. ( V \ { N } ) -> -. v e. ( E ` j ) ) )
99 98 imp 
 |-  ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( j e. dom E /\ ( E ` j ) = { N } ) ) /\ v e. ( V \ { N } ) ) -> -. v e. ( E ` j ) )
100 99 intnand 
 |-  ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( j e. dom E /\ ( E ` j ) = { N } ) ) /\ v e. ( V \ { N } ) ) -> -. ( N e. ( E ` j ) /\ v e. ( E ` j ) ) )
101 100 intnand 
 |-  ( ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( j e. dom E /\ ( E ` j ) = { N } ) ) /\ v e. ( V \ { N } ) ) -> -. ( j e. dom E /\ ( N e. ( E ` j ) /\ v e. ( E ` j ) ) ) )
102 101 ralrimiva 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( j e. dom E /\ ( E ` j ) = { N } ) ) -> A. v e. ( V \ { N } ) -. ( j e. dom E /\ ( N e. ( E ` j ) /\ v e. ( E ` j ) ) ) )
103 eliun 
 |-  ( j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> E. v e. ( V \ { N } ) j e. { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
104 103 notbii 
 |-  ( -. j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> -. E. v e. ( V \ { N } ) j e. { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
105 ralnex 
 |-  ( A. v e. ( V \ { N } ) -. j e. { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> -. E. v e. ( V \ { N } ) j e. { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
106 fveq2 
 |-  ( i = j -> ( E ` i ) = ( E ` j ) )
107 106 eleq2d 
 |-  ( i = j -> ( N e. ( E ` i ) <-> N e. ( E ` j ) ) )
108 106 eleq2d 
 |-  ( i = j -> ( v e. ( E ` i ) <-> v e. ( E ` j ) ) )
109 107 108 anbi12d 
 |-  ( i = j -> ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) <-> ( N e. ( E ` j ) /\ v e. ( E ` j ) ) ) )
110 109 elrab 
 |-  ( j e. { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> ( j e. dom E /\ ( N e. ( E ` j ) /\ v e. ( E ` j ) ) ) )
111 110 notbii 
 |-  ( -. j e. { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> -. ( j e. dom E /\ ( N e. ( E ` j ) /\ v e. ( E ` j ) ) ) )
112 111 ralbii 
 |-  ( A. v e. ( V \ { N } ) -. j e. { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> A. v e. ( V \ { N } ) -. ( j e. dom E /\ ( N e. ( E ` j ) /\ v e. ( E ` j ) ) ) )
113 104 105 112 3bitr2i 
 |-  ( -. j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } <-> A. v e. ( V \ { N } ) -. ( j e. dom E /\ ( N e. ( E ` j ) /\ v e. ( E ` j ) ) ) )
114 102 113 sylibr 
 |-  ( ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) /\ ( j e. dom E /\ ( E ` j ) = { N } ) ) -> -. j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
115 114 ex 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( ( j e. dom E /\ ( E ` j ) = { N } ) -> -. j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) )
116 92 115 biimtrid 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( j e. { i e. dom E | ( E ` i ) = { N } } -> -. j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) )
117 116 ralrimiv 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> A. j e. { i e. dom E | ( E ` i ) = { N } } -. j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
118 disjr 
 |-  ( ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( E ` i ) = { N } } ) = (/) <-> A. j e. { i e. dom E | ( E ` i ) = { N } } -. j e. U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
119 117 118 sylibr 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( E ` i ) = { N } } ) = (/) )
120 hashun 
 |-  ( ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } e. Fin /\ { i e. dom E | ( E ` i ) = { N } } e. Fin /\ ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } i^i { i e. dom E | ( E ` i ) = { N } } ) = (/) ) -> ( # ` ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) ) = ( ( # ` U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) )
121 86 90 119 120 syl3anc 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( # ` ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) ) = ( ( # ` U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) )
122 1 2 edglnl 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) = { i e. dom E | N e. ( E ` i ) } )
123 122 3adant2 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) = { i e. dom E | N e. ( E ` i ) } )
124 123 fveq2d 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( # ` ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` { i e. dom E | N e. ( E ` i ) } ) )
125 83 121 124 3eqtr2d 
 |-  ( ( G e. UPGraph /\ ( V e. Fin /\ E e. Fin ) /\ N e. V ) -> ( sum_ v e. ( V \ { N } ) ( # ` { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } ) + ( # ` { i e. dom E | ( E ` i ) = { N } } ) ) = ( # ` { i e. dom E | N e. ( E ` i ) } ) )