Metamath Proof Explorer

Theorem nbuhgr2vtx1edgb

Description: If a hypergraph 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) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbgr2vtx1edg.v ⊢ V = Vtx ⁡ G
nbgr2vtx1edg.e ⊢ E = Edg ⁡ G
Assertion nbuhgr2vtx1edgb ⊢ G ∈ UHGraph ∧ 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 simpr ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V → a ∈ V ∧ b ∈ V
7 6 ancomd ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V → b ∈ V ∧ a ∈ V
8 7 ad2antrr ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → b ∈ V ∧ a ∈ V
9 id ⊢ a ≠ b → a ≠ b
10 9 necomd ⊢ a ≠ b → b ≠ a
11 10 adantr ⊢ a ≠ b ∧ V = a b → b ≠ a
12 11 ad2antlr ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → b ≠ a
13 prcom ⊢ a b = b a
14 13 eleq1i ⊢ a b ∈ E ↔ b a ∈ E
15 14 biimpi ⊢ a b ∈ E → b a ∈ E
16 sseq2 ⊢ e = b a → a b ⊆ e ↔ a b ⊆ b a
17 16 adantl ⊢ a b ∈ E ∧ e = b a → a b ⊆ e ↔ a b ⊆ b a
18 13 eqimssi ⊢ a b ⊆ b a
19 18 a1i ⊢ a b ∈ E → a b ⊆ b a
20 15 17 19 rspcedvd ⊢ a b ∈ E → ∃ e ∈ E a b ⊆ e
21 20 adantl ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → ∃ e ∈ E a b ⊆ e
22 1 2 nbgrel ⊢ b ∈ G NeighbVtx a ↔ b ∈ V ∧ a ∈ V ∧ b ≠ a ∧ ∃ e ∈ E a b ⊆ e
23 8 12 21 22 syl3anbrc ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → b ∈ G NeighbVtx a
24 6 ad2antrr ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → a ∈ V ∧ b ∈ V
25 simplrl ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → a ≠ b
26 id ⊢ a b ∈ E → a b ∈ E
27 sseq2 ⊢ e = a b → b a ⊆ e ↔ b a ⊆ a b
28 27 adantl ⊢ a b ∈ E ∧ e = a b → b a ⊆ e ↔ b a ⊆ a b
29 prcom ⊢ b a = a b
30 29 eqimssi ⊢ b a ⊆ a b
31 30 a1i ⊢ a b ∈ E → b a ⊆ a b
32 26 28 31 rspcedvd ⊢ a b ∈ E → ∃ e ∈ E b a ⊆ e
33 32 adantl ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → ∃ e ∈ E b a ⊆ e
34 1 2 nbgrel ⊢ a ∈ G NeighbVtx b ↔ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ ∃ e ∈ E b a ⊆ e
35 24 25 33 34 syl3anbrc ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → a ∈ G NeighbVtx b
36 23 35 jca ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ∧ a b ∈ E → b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b
37 36 ex ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b → a b ∈ E → b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b
38 1 2 nbuhgr2vtx1edgblem ⊢ G ∈ UHGraph ∧ V = a b ∧ a ∈ G NeighbVtx b → a b ∈ E
39 38 3exp ⊢ G ∈ UHGraph → V = a b → a ∈ G NeighbVtx b → a b ∈ E
40 39 adantr ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V → V = a b → a ∈ G NeighbVtx b → a b ∈ E
41 40 adantld ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V → a ≠ b ∧ V = a b → a ∈ G NeighbVtx b → a b ∈ E
42 41 imp ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b → a ∈ G NeighbVtx b → a b ∈ E
43 42 adantld ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b → b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b → a b ∈ E
44 37 43 impbid ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b → a b ∈ E ↔ b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b
45 eleq1 ⊢ V = a b → V ∈ E ↔ a b ∈ E
46 45 adantl ⊢ a ≠ b ∧ 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 vex ⊢ a ∈ V
52 vex ⊢ b ∈ V
53 sneq ⊢ v = a → v = a
54 53 difeq2d ⊢ v = a → a b ∖ v = a b ∖ a
55 oveq2 ⊢ v = a → G NeighbVtx v = G NeighbVtx a
56 55 eleq2d ⊢ v = a → n ∈ G NeighbVtx v ↔ n ∈ G NeighbVtx a
57 54 56 raleqbidv ⊢ v = a → ∀ n ∈ a b ∖ v n ∈ G NeighbVtx v ↔ ∀ n ∈ a b ∖ a n ∈ G NeighbVtx a
58 sneq ⊢ v = b → v = b
59 58 difeq2d ⊢ v = b → a b ∖ v = a b ∖ b
60 oveq2 ⊢ v = b → G NeighbVtx v = G NeighbVtx b
61 60 eleq2d ⊢ v = b → n ∈ G NeighbVtx v ↔ n ∈ G NeighbVtx b
62 59 61 raleqbidv ⊢ v = b → ∀ n ∈ a b ∖ v n ∈ G NeighbVtx v ↔ ∀ n ∈ a b ∖ b n ∈ G NeighbVtx b
63 51 52 57 62 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
64 difprsn1 ⊢ a ≠ b → a b ∖ a = b
65 64 raleqdv ⊢ a ≠ b → ∀ n ∈ a b ∖ a n ∈ G NeighbVtx a ↔ ∀ n ∈ b n ∈ G NeighbVtx a
66 eleq1 ⊢ n = b → n ∈ G NeighbVtx a ↔ b ∈ G NeighbVtx a
67 52 66 ralsn ⊢ ∀ n ∈ b n ∈ G NeighbVtx a ↔ b ∈ G NeighbVtx a
68 65 67 syl6bb ⊢ a ≠ b → ∀ n ∈ a b ∖ a n ∈ G NeighbVtx a ↔ b ∈ G NeighbVtx a
69 difprsn2 ⊢ a ≠ b → a b ∖ b = a
70 69 raleqdv ⊢ a ≠ b → ∀ n ∈ a b ∖ b n ∈ G NeighbVtx b ↔ ∀ n ∈ a n ∈ G NeighbVtx b
71 eleq1 ⊢ n = a → n ∈ G NeighbVtx b ↔ a ∈ G NeighbVtx b
72 51 71 ralsn ⊢ ∀ n ∈ a n ∈ G NeighbVtx b ↔ a ∈ G NeighbVtx b
73 70 72 syl6bb ⊢ a ≠ b → ∀ n ∈ a b ∖ b n ∈ G NeighbVtx b ↔ a ∈ G NeighbVtx b
74 68 73 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
75 63 74 syl5bb ⊢ a ≠ b → ∀ v ∈ a b ∀ n ∈ a b ∖ v n ∈ G NeighbVtx v ↔ b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b
76 50 75 sylan9bbr ⊢ a ≠ b ∧ V = a b → ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b
77 46 76 bibi12d ⊢ a ≠ b ∧ V = a b → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ a b ∈ E ↔ b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b
78 77 adantl ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ a b ∈ E ↔ b ∈ G NeighbVtx a ∧ a ∈ G NeighbVtx b
79 44 78 mpbird ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
80 79 ex ⊢ G ∈ UHGraph ∧ a ∈ V ∧ b ∈ V → a ≠ b ∧ V = a b → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
81 80 rexlimdvva ⊢ G ∈ UHGraph → ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ V = a b → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
82 5 81 syl5bi ⊢ G ∈ UHGraph → V = 2 → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
83 82 imp ⊢ G ∈ UHGraph ∧ V = 2 → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v