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=VtxG
nbgr2vtx1edg.e E=EdgG
Assertion nbuhgr2vtx1edgb GUHGraphV=2VEvVnVvnGNeighbVtxv

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v V=VtxG
2 nbgr2vtx1edg.e E=EdgG
3 1 fvexi VV
4 hash2prb VVV=2aVbVabV=ab
5 3 4 ax-mp V=2aVbVabV=ab
6 simpr GUHGraphaVbVaVbV
7 6 ancomd GUHGraphaVbVbVaV
8 7 ad2antrr GUHGraphaVbVabV=ababEbVaV
9 id abab
10 9 necomd abba
11 10 adantr abV=abba
12 11 ad2antlr GUHGraphaVbVabV=ababEba
13 prcom ab=ba
14 13 eleq1i abEbaE
15 14 biimpi abEbaE
16 sseq2 e=baabeabba
17 16 adantl abEe=baabeabba
18 13 eqimssi abba
19 18 a1i abEabba
20 15 17 19 rspcedvd abEeEabe
21 20 adantl GUHGraphaVbVabV=ababEeEabe
22 1 2 nbgrel bGNeighbVtxabVaVbaeEabe
23 8 12 21 22 syl3anbrc GUHGraphaVbVabV=ababEbGNeighbVtxa
24 6 ad2antrr GUHGraphaVbVabV=ababEaVbV
25 simplrl GUHGraphaVbVabV=ababEab
26 id abEabE
27 sseq2 e=abbaebaab
28 27 adantl abEe=abbaebaab
29 prcom ba=ab
30 29 eqimssi baab
31 30 a1i abEbaab
32 26 28 31 rspcedvd abEeEbae
33 32 adantl GUHGraphaVbVabV=ababEeEbae
34 1 2 nbgrel aGNeighbVtxbaVbVabeEbae
35 24 25 33 34 syl3anbrc GUHGraphaVbVabV=ababEaGNeighbVtxb
36 23 35 jca GUHGraphaVbVabV=ababEbGNeighbVtxaaGNeighbVtxb
37 36 ex GUHGraphaVbVabV=ababEbGNeighbVtxaaGNeighbVtxb
38 1 2 nbuhgr2vtx1edgblem GUHGraphV=abaGNeighbVtxbabE
39 38 3exp GUHGraphV=abaGNeighbVtxbabE
40 39 adantr GUHGraphaVbVV=abaGNeighbVtxbabE
41 40 adantld GUHGraphaVbVabV=abaGNeighbVtxbabE
42 41 imp GUHGraphaVbVabV=abaGNeighbVtxbabE
43 42 adantld GUHGraphaVbVabV=abbGNeighbVtxaaGNeighbVtxbabE
44 37 43 impbid GUHGraphaVbVabV=ababEbGNeighbVtxaaGNeighbVtxb
45 eleq1 V=abVEabE
46 45 adantl abV=abVEabE
47 id V=abV=ab
48 difeq1 V=abVv=abv
49 48 raleqdv V=abnVvnGNeighbVtxvnabvnGNeighbVtxv
50 47 49 raleqbidv V=abvVnVvnGNeighbVtxvvabnabvnGNeighbVtxv
51 vex aV
52 vex bV
53 sneq v=av=a
54 53 difeq2d v=aabv=aba
55 oveq2 v=aGNeighbVtxv=GNeighbVtxa
56 55 eleq2d v=anGNeighbVtxvnGNeighbVtxa
57 54 56 raleqbidv v=anabvnGNeighbVtxvnabanGNeighbVtxa
58 sneq v=bv=b
59 58 difeq2d v=babv=abb
60 oveq2 v=bGNeighbVtxv=GNeighbVtxb
61 60 eleq2d v=bnGNeighbVtxvnGNeighbVtxb
62 59 61 raleqbidv v=bnabvnGNeighbVtxvnabbnGNeighbVtxb
63 51 52 57 62 ralpr vabnabvnGNeighbVtxvnabanGNeighbVtxanabbnGNeighbVtxb
64 difprsn1 ababa=b
65 64 raleqdv abnabanGNeighbVtxanbnGNeighbVtxa
66 eleq1 n=bnGNeighbVtxabGNeighbVtxa
67 52 66 ralsn nbnGNeighbVtxabGNeighbVtxa
68 65 67 bitrdi abnabanGNeighbVtxabGNeighbVtxa
69 difprsn2 ababb=a
70 69 raleqdv abnabbnGNeighbVtxbnanGNeighbVtxb
71 eleq1 n=anGNeighbVtxbaGNeighbVtxb
72 51 71 ralsn nanGNeighbVtxbaGNeighbVtxb
73 70 72 bitrdi abnabbnGNeighbVtxbaGNeighbVtxb
74 68 73 anbi12d abnabanGNeighbVtxanabbnGNeighbVtxbbGNeighbVtxaaGNeighbVtxb
75 63 74 syl5bb abvabnabvnGNeighbVtxvbGNeighbVtxaaGNeighbVtxb
76 50 75 sylan9bbr abV=abvVnVvnGNeighbVtxvbGNeighbVtxaaGNeighbVtxb
77 46 76 bibi12d abV=abVEvVnVvnGNeighbVtxvabEbGNeighbVtxaaGNeighbVtxb
78 77 adantl GUHGraphaVbVabV=abVEvVnVvnGNeighbVtxvabEbGNeighbVtxaaGNeighbVtxb
79 44 78 mpbird GUHGraphaVbVabV=abVEvVnVvnGNeighbVtxv
80 79 ex GUHGraphaVbVabV=abVEvVnVvnGNeighbVtxv
81 80 rexlimdvva GUHGraphaVbVabV=abVEvVnVvnGNeighbVtxv
82 5 81 syl5bi GUHGraphV=2VEvVnVvnGNeighbVtxv
83 82 imp GUHGraphV=2VEvVnVvnGNeighbVtxv