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 bitrdi 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 bitrdi 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