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 ∖ 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 iunrab ⊢ ⋃ v ∈ V ∖ N i ∈ dom ⁡ E | N ∈ E ⁡ i ∧ v ∈ E ⁡ i = i ∈ dom ⁡ E | ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i
4 3 a1i ⊢ G ∈ UPGraph ∧ N ∈ V → ⋃ v ∈ V ∖ N i ∈ dom ⁡ E | N ∈ E ⁡ i ∧ v ∈ E ⁡ i = i ∈ dom ⁡ E | ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i
5 4 uneq1d ⊢ 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 | ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∪ i ∈ dom ⁡ E | E ⁡ i = N
6 unrab ⊢ i ∈ dom ⁡ E | ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∪ i ∈ dom ⁡ E | E ⁡ i = N = i ∈ dom ⁡ E | ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N
7 simpl ⊢ N ∈ E ⁡ i ∧ v ∈ E ⁡ i → N ∈ E ⁡ i
8 7 rexlimivw ⊢ ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i → N ∈ E ⁡ i
9 8 a1i ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E → ∃ v ∈ V ∖ N N ∈ 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 ∖ N N ∈ 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 ∈ V E ⁡ i = n m
23 22 ex ⊢ G ∈ UPGraph → E ⁡ i ∈ Edg ⁡ G → ∃ n ∈ V ∃ m ∈ V E ⁡ i = n m
24 23 ad2antrr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E → E ⁡ i ∈ Edg ⁡ G → ∃ n ∈ V ∃ m ∈ V E ⁡ i = n m
25 dfsn2 ⊢ n = n n
26 25 eqcomi ⊢ n n = 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 syl5eq ⊢ N ∈ n → n n = N
32 31 26 eleq2s ⊢ N ∈ n n → n n = N
33 preq2 ⊢ m = n → n m = n n
34 33 eleq2d ⊢ m = n → N ∈ n m ↔ N ∈ n n
35 33 eqeq1d ⊢ m = n → n m = N ↔ n n = N
36 34 35 imbi12d ⊢ m = n → N ∈ n m → n m = N ↔ N ∈ n n → n n = N
37 32 36 mpbiri ⊢ m = n → N ∈ n m → n m = N
38 37 imp ⊢ m = n ∧ N ∈ n m → n m = N
39 38 olcd ⊢ m = n ∧ N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
40 39 expcom ⊢ N ∈ n m → m = n → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
41 40 3ad2ant3 ⊢ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → m = n → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
42 41 com12 ⊢ m = n → N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
43 simpr3 ⊢ m ≠ n ∧ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → N ∈ n m
44 simpl ⊢ m ≠ n ∧ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → m ≠ n
45 44 necomd ⊢ m ≠ n ∧ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → n ≠ m
46 simpr2 ⊢ m ≠ n ∧ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → n ∈ V ∧ m ∈ V
47 prproe ⊢ N ∈ n m ∧ n ≠ m ∧ n ∈ V ∧ m ∈ V → ∃ v ∈ V ∖ N v ∈ n m
48 43 45 46 47 syl3anc ⊢ m ≠ n ∧ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → ∃ v ∈ V ∖ N v ∈ n m
49 r19.42v ⊢ ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ↔ N ∈ n m ∧ ∃ v ∈ V ∖ N v ∈ n m
50 43 48 49 sylanbrc ⊢ m ≠ n ∧ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m
51 50 orcd ⊢ m ≠ n ∧ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
52 51 ex ⊢ m ≠ n → N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
53 42 52 pm2.61ine ⊢ N ∈ V ∧ n ∈ V ∧ m ∈ V ∧ N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
54 53 3exp ⊢ N ∈ V → n ∈ V ∧ m ∈ V → N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
55 54 ad2antlr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E → n ∈ V ∧ m ∈ V → N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
56 55 imp ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E ∧ n ∈ V ∧ m ∈ V → N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
57 eleq2 ⊢ E ⁡ i = n m → N ∈ E ⁡ i ↔ N ∈ n m
58 eleq2 ⊢ E ⁡ i = n m → v ∈ E ⁡ i ↔ v ∈ n m
59 57 58 anbi12d ⊢ E ⁡ i = n m → N ∈ E ⁡ i ∧ v ∈ E ⁡ i ↔ N ∈ n m ∧ v ∈ n m
60 59 rexbidv ⊢ E ⁡ i = n m → ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ↔ ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m
61 eqeq1 ⊢ E ⁡ i = n m → E ⁡ i = N ↔ n m = N
62 60 61 orbi12d ⊢ E ⁡ i = n m → ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N ↔ ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
63 57 62 imbi12d ⊢ E ⁡ i = n m → N ∈ E ⁡ i → ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N ↔ N ∈ n m → ∃ v ∈ V ∖ N N ∈ n m ∧ v ∈ n m ∨ n m = N
64 56 63 syl5ibrcom ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E ∧ n ∈ V ∧ m ∈ V → E ⁡ i = n m → N ∈ E ⁡ i → ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N
65 64 rexlimdvva ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E → ∃ n ∈ V ∃ m ∈ V E ⁡ i = n m → N ∈ E ⁡ i → ∃ v ∈ V ∖ N N ∈ 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 ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N
67 20 66 mpd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E → N ∈ E ⁡ i → ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N
68 14 67 impbid ⊢ G ∈ UPGraph ∧ N ∈ V ∧ i ∈ dom ⁡ E → ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N ↔ N ∈ E ⁡ i
69 68 rabbidva ⊢ G ∈ UPGraph ∧ N ∈ V → i ∈ dom ⁡ E | ∃ v ∈ V ∖ N N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∨ E ⁡ i = N = i ∈ dom ⁡ E | N ∈ E ⁡ i
70 6 69 syl5eq ⊢ G ∈ UPGraph ∧ N ∈ V → i ∈ dom ⁡ E | ∃ v ∈ V ∖ N N ∈ 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 ∖ N i ∈ dom ⁡ E | N ∈ E ⁡ i ∧ v ∈ E ⁡ i ∪ i ∈ dom ⁡ E | E ⁡ i = N = i ∈ dom ⁡ E | N ∈ E ⁡ i