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 ∖ v n ∈ G NeighbVtx v

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