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 ∈ UPGraph ∧ V ∈ Fin ∧ E ∈ Fin ∧ N ∈ V → ∑ v ∈ V ∖ N i ∈ dom ⁡ E | N ∈ E ⁡ i ∧ v ∈ E ⁡ i + i ∈ dom ⁡ E | E ⁡ i = N = i ∈ dom ⁡ E | N ∈ E ⁡ i

Proof

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