Metamath Proof Explorer

Theorem nbupgrel

Description: A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢ V = Vtx ⁡ G
nbuhgr.e ⊢ E = Edg ⁡ G
Assertion nbupgrel ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V ∧ N ≠ K → N ∈ G NeighbVtx K ↔ N K ∈ E

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ V = Vtx ⁡ G
2 nbuhgr.e ⊢ E = Edg ⁡ G
3 1 2 nbupgr ⊢ G ∈ UPGraph ∧ K ∈ V → G NeighbVtx K = n ∈ V ∖ K | K n ∈ E
4 3 eleq2d ⊢ G ∈ UPGraph ∧ K ∈ V → N ∈ G NeighbVtx K ↔ N ∈ n ∈ V ∖ K | K n ∈ E
5 preq2 ⊢ n = N → K n = K N
6 5 eleq1d ⊢ n = N → K n ∈ E ↔ K N ∈ E
7 6 elrab ⊢ N ∈ n ∈ V ∖ K | K n ∈ E ↔ N ∈ V ∖ K ∧ K N ∈ E
8 4 7 syl6bb ⊢ G ∈ UPGraph ∧ K ∈ V → N ∈ G NeighbVtx K ↔ N ∈ V ∖ K ∧ K N ∈ E
9 8 adantr ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V ∧ N ≠ K → N ∈ G NeighbVtx K ↔ N ∈ V ∖ K ∧ K N ∈ E
10 eldifsn ⊢ N ∈ V ∖ K ↔ N ∈ V ∧ N ≠ K
11 10 biimpri ⊢ N ∈ V ∧ N ≠ K → N ∈ V ∖ K
12 11 adantl ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V ∧ N ≠ K → N ∈ V ∖ K
13 12 biantrurd ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V ∧ N ≠ K → K N ∈ E ↔ N ∈ V ∖ K ∧ K N ∈ E
14 prcom ⊢ K N = N K
15 14 eleq1i ⊢ K N ∈ E ↔ N K ∈ E
16 15 a1i ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V ∧ N ≠ K → K N ∈ E ↔ N K ∈ E
17 9 13 16 3bitr2d ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V ∧ N ≠ K → N ∈ G NeighbVtx K ↔ N K ∈ E