Metamath Proof Explorer

Theorem nbupgr

Description: The set of neighbors of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020) (Proof shortened by AV, 30-Dec-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢ V = Vtx ⁡ G
nbuhgr.e ⊢ E = Edg ⁡ G
Assertion nbupgr ⊢ G ∈ UPGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | N n ∈ E

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ V = Vtx ⁡ G
2 nbuhgr.e ⊢ E = Edg ⁡ G
3 1 2 nbgrval ⊢ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e
4 3 adantl ⊢ G ∈ UPGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e
5 simp-4l ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E ∧ N n ⊆ e → G ∈ UPGraph
6 simpr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E → e ∈ E
7 6 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E ∧ N n ⊆ e → e ∈ E
8 simpr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E ∧ N n ⊆ e → N n ⊆ e
9 simpr ⊢ G ∈ UPGraph ∧ N ∈ V → N ∈ V
10 9 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N → N ∈ V
11 vex ⊢ n ∈ V
12 11 a1i ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N → n ∈ V
13 eldifsn ⊢ n ∈ V ∖ N ↔ n ∈ V ∧ n ≠ N
14 simpr ⊢ n ∈ V ∧ n ≠ N → n ≠ N
15 14 necomd ⊢ n ∈ V ∧ n ≠ N → N ≠ n
16 13 15 sylbi ⊢ n ∈ V ∖ N → N ≠ n
17 16 adantl ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N → N ≠ n
18 10 12 17 3jca ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N → N ∈ V ∧ n ∈ V ∧ N ≠ n
19 18 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E → N ∈ V ∧ n ∈ V ∧ N ≠ n
20 19 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E ∧ N n ⊆ e → N ∈ V ∧ n ∈ V ∧ N ≠ n
21 1 2 upgredgpr ⊢ G ∈ UPGraph ∧ e ∈ E ∧ N n ⊆ e ∧ N ∈ V ∧ n ∈ V ∧ N ≠ n → N n = e
22 5 7 8 20 21 syl31anc ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E ∧ N n ⊆ e → N n = e
23 22 ex ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E → N n ⊆ e → N n = e
24 eleq1 ⊢ N n = e → N n ∈ E ↔ e ∈ E
25 24 biimprd ⊢ N n = e → e ∈ E → N n ∈ E
26 23 6 25 syl6ci ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ e ∈ E → N n ⊆ e → N n ∈ E
27 26 rexlimdva ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N → ∃ e ∈ E N n ⊆ e → N n ∈ E
28 simpr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ N n ∈ E → N n ∈ E
29 sseq2 ⊢ e = N n → N n ⊆ e ↔ N n ⊆ N n
30 29 adantl ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ N n ∈ E ∧ e = N n → N n ⊆ e ↔ N n ⊆ N n
31 ssidd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ N n ∈ E → N n ⊆ N n
32 28 30 31 rspcedvd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N ∧ N n ∈ E → ∃ e ∈ E N n ⊆ e
33 32 ex ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N → N n ∈ E → ∃ e ∈ E N n ⊆ e
34 27 33 impbid ⊢ G ∈ UPGraph ∧ N ∈ V ∧ n ∈ V ∖ N → ∃ e ∈ E N n ⊆ e ↔ N n ∈ E
35 34 rabbidva ⊢ G ∈ UPGraph ∧ N ∈ V → n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e = n ∈ V ∖ N | N n ∈ E
36 4 35 eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | N n ∈ E