Metamath Proof Explorer

Theorem nbgr2vtx1edg

Description: If a graph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020) (Revised by AV, 25-Mar-2021) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbgr2vtx1edg.v ⊢V=Vtx⁡G
nbgr2vtx1edg.e ⊢E=Edg⁡G
Assertion nbgr2vtx1edg ⊢V=2∧V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v ⊢V=Vtx⁡G
2 nbgr2vtx1edg.e ⊢E=Edg⁡G
3 1 fvexi ⊢V∈V
4 hash2prb ⊢V∈V→V=2↔∃a∈V∃b∈Va≠b∧V=ab
5 3 4 ax-mp ⊢V=2↔∃a∈V∃b∈Va≠b∧V=ab
6 simpll ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→a∈V∧b∈V
7 6 ancomd ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→b∈V∧a∈V
8 simpl ⊢a≠b∧V=ab→a≠b
9 8 necomd ⊢a≠b∧V=ab→b≠a
10 9 ad2antlr ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→b≠a
11 id ⊢ab∈E→ab∈E
12 sseq2 ⊢e=ab→ab⊆e↔ab⊆ab
13 12 adantl ⊢ab∈E∧e=ab→ab⊆e↔ab⊆ab
14 ssidd ⊢ab∈E→ab⊆ab
15 11 13 14 rspcedvd ⊢ab∈E→∃e∈Eab⊆e
16 15 adantl ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→∃e∈Eab⊆e
17 1 2 nbgrel ⊢b∈GNeighbVtxa↔b∈V∧a∈V∧b≠a∧∃e∈Eab⊆e
18 7 10 16 17 syl3anbrc ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→b∈GNeighbVtxa
19 8 ad2antlr ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→a≠b
20 sseq2 ⊢e=ab→ba⊆e↔ba⊆ab
21 20 adantl ⊢ab∈E∧e=ab→ba⊆e↔ba⊆ab
22 prcom ⊢ba=ab
23 22 eqimssi ⊢ba⊆ab
24 23 a1i ⊢ab∈E→ba⊆ab
25 11 21 24 rspcedvd ⊢ab∈E→∃e∈Eba⊆e
26 25 adantl ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→∃e∈Eba⊆e
27 1 2 nbgrel ⊢a∈GNeighbVtxb↔a∈V∧b∈V∧a≠b∧∃e∈Eba⊆e
28 6 19 26 27 syl3anbrc ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→a∈GNeighbVtxb
29 difprsn1 ⊢a≠b→ab∖a=b
30 29 raleqdv ⊢a≠b→∀n∈ab∖an∈GNeighbVtxa↔∀n∈bn∈GNeighbVtxa
31 vex ⊢b∈V
32 eleq1 ⊢n=b→n∈GNeighbVtxa↔b∈GNeighbVtxa
33 31 32 ralsn ⊢∀n∈bn∈GNeighbVtxa↔b∈GNeighbVtxa
34 30 33 bitrdi ⊢a≠b→∀n∈ab∖an∈GNeighbVtxa↔b∈GNeighbVtxa
35 difprsn2 ⊢a≠b→ab∖b=a
36 35 raleqdv ⊢a≠b→∀n∈ab∖bn∈GNeighbVtxb↔∀n∈an∈GNeighbVtxb
37 vex ⊢a∈V
38 eleq1 ⊢n=a→n∈GNeighbVtxb↔a∈GNeighbVtxb
39 37 38 ralsn ⊢∀n∈an∈GNeighbVtxb↔a∈GNeighbVtxb
40 36 39 bitrdi ⊢a≠b→∀n∈ab∖bn∈GNeighbVtxb↔a∈GNeighbVtxb
41 34 40 anbi12d ⊢a≠b→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb↔b∈GNeighbVtxa∧a∈GNeighbVtxb
42 41 adantr ⊢a≠b∧V=ab→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb↔b∈GNeighbVtxa∧a∈GNeighbVtxb
43 42 ad2antlr ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb↔b∈GNeighbVtxa∧a∈GNeighbVtxb
44 18 28 43 mpbir2and ⊢a∈V∧b∈V∧a≠b∧V=ab∧ab∈E→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb
45 44 ex ⊢a∈V∧b∈V∧a≠b∧V=ab→ab∈E→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb
46 eleq1 ⊢V=ab→V∈E↔ab∈E
47 id ⊢V=ab→V=ab
48 difeq1 ⊢V=ab→V∖v=ab∖v
49 48 raleqdv ⊢V=ab→∀n∈V∖vn∈GNeighbVtxv↔∀n∈ab∖vn∈GNeighbVtxv
50 47 49 raleqbidv ⊢V=ab→∀v∈V∀n∈V∖vn∈GNeighbVtxv↔∀v∈ab∀n∈ab∖vn∈GNeighbVtxv
51 sneq ⊢v=a→v=a
52 51 difeq2d ⊢v=a→ab∖v=ab∖a
53 oveq2 ⊢v=a→GNeighbVtxv=GNeighbVtxa
54 53 eleq2d ⊢v=a→n∈GNeighbVtxv↔n∈GNeighbVtxa
55 52 54 raleqbidv ⊢v=a→∀n∈ab∖vn∈GNeighbVtxv↔∀n∈ab∖an∈GNeighbVtxa
56 sneq ⊢v=b→v=b
57 56 difeq2d ⊢v=b→ab∖v=ab∖b
58 oveq2 ⊢v=b→GNeighbVtxv=GNeighbVtxb
59 58 eleq2d ⊢v=b→n∈GNeighbVtxv↔n∈GNeighbVtxb
60 57 59 raleqbidv ⊢v=b→∀n∈ab∖vn∈GNeighbVtxv↔∀n∈ab∖bn∈GNeighbVtxb
61 37 31 55 60 ralpr ⊢∀v∈ab∀n∈ab∖vn∈GNeighbVtxv↔∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb
62 50 61 bitrdi ⊢V=ab→∀v∈V∀n∈V∖vn∈GNeighbVtxv↔∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb
63 46 62 imbi12d ⊢V=ab→V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv↔ab∈E→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb
64 63 adantl ⊢a≠b∧V=ab→V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv↔ab∈E→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb
65 64 adantl ⊢a∈V∧b∈V∧a≠b∧V=ab→V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv↔ab∈E→∀n∈ab∖an∈GNeighbVtxa∧∀n∈ab∖bn∈GNeighbVtxb
66 45 65 mpbird ⊢a∈V∧b∈V∧a≠b∧V=ab→V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv
67 66 ex ⊢a∈V∧b∈V→a≠b∧V=ab→V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv
68 67 rexlimivv ⊢∃a∈V∃b∈Va≠b∧V=ab→V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv
69 5 68 sylbi ⊢V=2→V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv
70 69 imp ⊢V=2∧V∈E→∀v∈V∀n∈V∖vn∈GNeighbVtxv