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∖Ni∈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∈VE⁡i=mn
21 18 20 syldan ⊢G∈UPGraph∧i∈dom⁡E→∃m∈V∃n∈VE⁡i=mn
22 21 ex ⊢G∈UPGraph→i∈dom⁡E→∃m∈V∃n∈VE⁡i=mn
23 22 3ad2ant1 ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→i∈dom⁡E→∃m∈V∃n∈VE⁡i=mn
24 23 adantr ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V∧v∈V∖N∧w∈V∖N→i∈dom⁡E→∃m∈V∃n∈VE⁡i=mn
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∈VE⁡i=mn
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∈VE⁡i=mn
27 eldifsni ⊢v∈V∖N→v≠N
28 eldifsni ⊢w∈V∖N→w≠N
29 3elpr2eq ⊢N∈mn∧v∈mn∧w∈mn∧v≠N∧w≠N→v=w
30 29 expcom ⊢v≠N∧w≠N→N∈mn∧v∈mn∧w∈mn→v=w
31 30 3expd ⊢v≠N∧w≠N→N∈mn→v∈mn→w∈mn→v=w
32 31 com23 ⊢v≠N∧w≠N→v∈mn→N∈mn→w∈mn→v=w
33 32 3imp ⊢v≠N∧w≠N∧v∈mn∧N∈mn→w∈mn→v=w
34 33 con3d ⊢v≠N∧w≠N∧v∈mn∧N∈mn→¬v=w→¬w∈mn
35 34 3exp ⊢v≠N∧w≠N→v∈mn→N∈mn→¬v=w→¬w∈mn
36 35 com24 ⊢v≠N∧w≠N→¬v=w→N∈mn→v∈mn→¬w∈mn
37 36 imp ⊢v≠N∧w≠N∧¬v=w→N∈mn→v∈mn→¬w∈mn
38 eleq2 ⊢E⁡i=mn→N∈E⁡i↔N∈mn
39 eleq2 ⊢E⁡i=mn→v∈E⁡i↔v∈mn
40 eleq2 ⊢E⁡i=mn→w∈E⁡i↔w∈mn
41 40 notbid ⊢E⁡i=mn→¬w∈E⁡i↔¬w∈mn
42 39 41 imbi12d ⊢E⁡i=mn→v∈E⁡i→¬w∈E⁡i↔v∈mn→¬w∈mn
43 38 42 imbi12d ⊢E⁡i=mn→N∈E⁡i→v∈E⁡i→¬w∈E⁡i↔N∈mn→v∈mn→¬w∈mn
44 37 43 syl5ibrcom ⊢v≠N∧w≠N∧¬v=w→E⁡i=mn→N∈E⁡i→v∈E⁡i→¬w∈E⁡i
45 44 adantr ⊢v≠N∧w≠N∧¬v=w∧m∈V∧n∈V→E⁡i=mn→N∈E⁡i→v∈E⁡i→¬w∈E⁡i
46 45 rexlimdvva ⊢v≠N∧w≠N∧¬v=w→∃m∈V∃n∈VE⁡i=mn→N∈E⁡i→v∈E⁡i→¬w∈E⁡i
47 46 ex ⊢v≠N∧w≠N→¬v=w→∃m∈V∃n∈VE⁡i=mn→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∈VE⁡i=mn→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∈VE⁡i=mn→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∈VE⁡i=mn→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∈VE⁡i=mn→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 biimtrrid ⊢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 biimtrrid ⊢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∖Nv=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 ⊢Disjv∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i↔∀v∈V∖N∀w∈V∖Nv=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→Disjv∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i
81 5 11 80 hashiun ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i=∑v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i
82 81 eqcomd ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→∑v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i=⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i
83 82 oveq1d ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→∑v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i+i∈dom⁡E|E⁡i=N=⋃v∈V∖Ni∈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∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∈Fin
85 iunfi ⊢V∖N∈Fin∧∀v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∈Fin→⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∈Fin
86 5 84 85 syl2anc ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→⋃v∈V∖Ni∈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 imbitrrid ⊢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∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i↔∃v∈V∖Nj∈i∈dom⁡E|N∈E⁡i∧v∈E⁡i
104 103 notbii ⊢¬j∈⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i↔¬∃v∈V∖Nj∈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∖Nj∈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∖Ni∈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∖Ni∈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∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i
116 92 115 biimtrid ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→j∈i∈dom⁡E|E⁡i=N→¬j∈⋃v∈V∖Ni∈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∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i
118 disjr ⊢⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∩i∈dom⁡E|E⁡i=N=∅↔∀j∈i∈dom⁡E|E⁡i=N¬j∈⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i
119 117 118 sylibr ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∩i∈dom⁡E|E⁡i=N=∅
120 hashun ⊢⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∈Fin∧i∈dom⁡E|E⁡i=N∈Fin∧⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∩i∈dom⁡E|E⁡i=N=∅→⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∪i∈dom⁡E|E⁡i=N=⋃v∈V∖Ni∈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∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∪i∈dom⁡E|E⁡i=N=⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i+i∈dom⁡E|E⁡i=N
122 1 2 edglnl ⊢G∈UPGraph∧N∈V→⋃v∈V∖Ni∈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∖Ni∈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∖Ni∈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∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i+i∈dom⁡E|E⁡i=N=i∈dom⁡E|N∈E⁡i