Metamath Proof Explorer

Theorem edglnl

Description: The edges incident with a vertex N are the edges joining N with other vertices and the loops on N in a pseudograph. (Contributed by AV, 18-Dec-2021)

Ref Expression
Hypotheses edglnl.v ⊢V=Vtx⁡G
edglnl.e ⊢E=iEdg⁡G
Assertion 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

Proof

Step Hyp Ref Expression
1 edglnl.v ⊢V=Vtx⁡G
2 edglnl.e ⊢E=iEdg⁡G
3 iunrab ⊢⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i=i∈dom⁡E|∃v∈V∖NN∈E⁡i∧v∈E⁡i
4 3 a1i ⊢G∈UPGraph∧N∈V→⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i=i∈dom⁡E|∃v∈V∖NN∈E⁡i∧v∈E⁡i
5 4 uneq1d ⊢G∈UPGraph∧N∈V→⋃v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i∪i∈dom⁡E|E⁡i=N=i∈dom⁡E|∃v∈V∖NN∈E⁡i∧v∈E⁡i∪i∈dom⁡E|E⁡i=N
6 unrab ⊢i∈dom⁡E|∃v∈V∖NN∈E⁡i∧v∈E⁡i∪i∈dom⁡E|E⁡i=N=i∈dom⁡E|∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N
7 simpl ⊢N∈E⁡i∧v∈E⁡i→N∈E⁡i
8 7 rexlimivw ⊢∃v∈V∖NN∈E⁡i∧v∈E⁡i→N∈E⁡i
9 8 a1i ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→∃v∈V∖NN∈E⁡i∧v∈E⁡i→N∈E⁡i
10 snidg ⊢N∈V→N∈N
11 10 ad2antlr ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→N∈N
12 eleq2 ⊢E⁡i=N→N∈E⁡i↔N∈N
13 11 12 syl5ibrcom ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→E⁡i=N→N∈E⁡i
14 9 13 jaod ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N→N∈E⁡i
15 upgruhgr ⊢G∈UPGraph→G∈UHGraph
16 2 uhgrfun ⊢G∈UHGraph→Fun⁡E
17 15 16 syl ⊢G∈UPGraph→Fun⁡E
18 17 adantr ⊢G∈UPGraph∧N∈V→Fun⁡E
19 2 iedgedg ⊢Fun⁡E∧i∈dom⁡E→E⁡i∈Edg⁡G
20 18 19 sylan ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→E⁡i∈Edg⁡G
21 eqid ⊢Edg⁡G=Edg⁡G
22 1 21 upgredg ⊢G∈UPGraph∧E⁡i∈Edg⁡G→∃n∈V∃m∈VE⁡i=nm
23 22 ex ⊢G∈UPGraph→E⁡i∈Edg⁡G→∃n∈V∃m∈VE⁡i=nm
24 23 ad2antrr ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→E⁡i∈Edg⁡G→∃n∈V∃m∈VE⁡i=nm
25 dfsn2 ⊢n=nn
26 25 eqcomi ⊢nn=n
27 elsni ⊢N∈n→N=n
28 sneq ⊢N=n→N=n
29 28 eqcomd ⊢N=n→n=N
30 27 29 syl ⊢N∈n→n=N
31 26 30 eqtrid ⊢N∈n→nn=N
32 31 26 eleq2s ⊢N∈nn→nn=N
33 preq2 ⊢m=n→nm=nn
34 33 eleq2d ⊢m=n→N∈nm↔N∈nn
35 33 eqeq1d ⊢m=n→nm=N↔nn=N
36 34 35 imbi12d ⊢m=n→N∈nm→nm=N↔N∈nn→nn=N
37 32 36 mpbiri ⊢m=n→N∈nm→nm=N
38 37 imp ⊢m=n∧N∈nm→nm=N
39 38 olcd ⊢m=n∧N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
40 39 expcom ⊢N∈nm→m=n→∃v∈V∖NN∈nm∧v∈nm∨nm=N
41 40 3ad2ant3 ⊢N∈V∧n∈V∧m∈V∧N∈nm→m=n→∃v∈V∖NN∈nm∧v∈nm∨nm=N
42 41 com12 ⊢m=n→N∈V∧n∈V∧m∈V∧N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
43 simpr3 ⊢m≠n∧N∈V∧n∈V∧m∈V∧N∈nm→N∈nm
44 simpl ⊢m≠n∧N∈V∧n∈V∧m∈V∧N∈nm→m≠n
45 44 necomd ⊢m≠n∧N∈V∧n∈V∧m∈V∧N∈nm→n≠m
46 simpr2 ⊢m≠n∧N∈V∧n∈V∧m∈V∧N∈nm→n∈V∧m∈V
47 prproe ⊢N∈nm∧n≠m∧n∈V∧m∈V→∃v∈V∖Nv∈nm
48 43 45 46 47 syl3anc ⊢m≠n∧N∈V∧n∈V∧m∈V∧N∈nm→∃v∈V∖Nv∈nm
49 r19.42v ⊢∃v∈V∖NN∈nm∧v∈nm↔N∈nm∧∃v∈V∖Nv∈nm
50 43 48 49 sylanbrc ⊢m≠n∧N∈V∧n∈V∧m∈V∧N∈nm→∃v∈V∖NN∈nm∧v∈nm
51 50 orcd ⊢m≠n∧N∈V∧n∈V∧m∈V∧N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
52 51 ex ⊢m≠n→N∈V∧n∈V∧m∈V∧N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
53 42 52 pm2.61ine ⊢N∈V∧n∈V∧m∈V∧N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
54 53 3exp ⊢N∈V→n∈V∧m∈V→N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
55 54 ad2antlr ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→n∈V∧m∈V→N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
56 55 imp ⊢G∈UPGraph∧N∈V∧i∈dom⁡E∧n∈V∧m∈V→N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
57 eleq2 ⊢E⁡i=nm→N∈E⁡i↔N∈nm
58 eleq2 ⊢E⁡i=nm→v∈E⁡i↔v∈nm
59 57 58 anbi12d ⊢E⁡i=nm→N∈E⁡i∧v∈E⁡i↔N∈nm∧v∈nm
60 59 rexbidv ⊢E⁡i=nm→∃v∈V∖NN∈E⁡i∧v∈E⁡i↔∃v∈V∖NN∈nm∧v∈nm
61 eqeq1 ⊢E⁡i=nm→E⁡i=N↔nm=N
62 60 61 orbi12d ⊢E⁡i=nm→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N↔∃v∈V∖NN∈nm∧v∈nm∨nm=N
63 57 62 imbi12d ⊢E⁡i=nm→N∈E⁡i→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N↔N∈nm→∃v∈V∖NN∈nm∧v∈nm∨nm=N
64 56 63 syl5ibrcom ⊢G∈UPGraph∧N∈V∧i∈dom⁡E∧n∈V∧m∈V→E⁡i=nm→N∈E⁡i→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N
65 64 rexlimdvva ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→∃n∈V∃m∈VE⁡i=nm→N∈E⁡i→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N
66 24 65 syld ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→E⁡i∈Edg⁡G→N∈E⁡i→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N
67 20 66 mpd ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→N∈E⁡i→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N
68 14 67 impbid ⊢G∈UPGraph∧N∈V∧i∈dom⁡E→∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N↔N∈E⁡i
69 68 rabbidva ⊢G∈UPGraph∧N∈V→i∈dom⁡E|∃v∈V∖NN∈E⁡i∧v∈E⁡i∨E⁡i=N=i∈dom⁡E|N∈E⁡i
70 6 69 eqtrid ⊢G∈UPGraph∧N∈V→i∈dom⁡E|∃v∈V∖NN∈E⁡i∧v∈E⁡i∪i∈dom⁡E|E⁡i=N=i∈dom⁡E|N∈E⁡i
71 5 70 eqtrd ⊢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