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 e. UHGraph /\ ( # ` V ) = 2 ) -> ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v
 |-  V = ( Vtx ` G )
2 nbgr2vtx1edg.e
 |-  E = ( Edg ` G )
3 1 fvexi
 |-  V e. _V
4 hash2prb
 |-  ( V e. _V -> ( ( # ` V ) = 2 <-> E. a e. V E. b e. V ( a =/= b /\ V = { a , b } ) ) )
5 3 4 ax-mp
 |-  ( ( # ` V ) = 2 <-> E. a e. V E. b e. V ( a =/= b /\ V = { a , b } ) )
6 simpr
 |-  ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) -> ( a e. V /\ b e. V ) )
7 6 ancomd
 |-  ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) -> ( b e. V /\ a e. V ) )
8 7 ad2antrr
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> ( b e. V /\ a e. 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 e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> b =/= a )
13 prcom
 |-  { a , b } = { b , a }
14 13 eleq1i
 |-  ( { a , b } e. E <-> { b , a } e. E )
15 14 biimpi
 |-  ( { a , b } e. E -> { b , a } e. E )
16 sseq2
 |-  ( e = { b , a } -> ( { a , b } C_ e <-> { a , b } C_ { b , a } ) )
17 16 adantl
 |-  ( ( { a , b } e. E /\ e = { b , a } ) -> ( { a , b } C_ e <-> { a , b } C_ { b , a } ) )
18 13 eqimssi
 |-  { a , b } C_ { b , a }
19 18 a1i
 |-  ( { a , b } e. E -> { a , b } C_ { b , a } )
20 15 17 19 rspcedvd
 |-  ( { a , b } e. E -> E. e e. E { a , b } C_ e )
21 20 adantl
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> E. e e. E { a , b } C_ e )
22 1 2 nbgrel
 |-  ( b e. ( G NeighbVtx a ) <-> ( ( b e. V /\ a e. V ) /\ b =/= a /\ E. e e. E { a , b } C_ e ) )
23 8 12 21 22 syl3anbrc
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> b e. ( G NeighbVtx a ) )
24 6 ad2antrr
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> ( a e. V /\ b e. V ) )
25 simplrl
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> a =/= b )
26 id
 |-  ( { a , b } e. E -> { a , b } e. E )
27 sseq2
 |-  ( e = { a , b } -> ( { b , a } C_ e <-> { b , a } C_ { a , b } ) )
28 27 adantl
 |-  ( ( { a , b } e. E /\ e = { a , b } ) -> ( { b , a } C_ e <-> { b , a } C_ { a , b } ) )
29 prcom
 |-  { b , a } = { a , b }
30 29 eqimssi
 |-  { b , a } C_ { a , b }
31 30 a1i
 |-  ( { a , b } e. E -> { b , a } C_ { a , b } )
32 26 28 31 rspcedvd
 |-  ( { a , b } e. E -> E. e e. E { b , a } C_ e )
33 32 adantl
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> E. e e. E { b , a } C_ e )
34 1 2 nbgrel
 |-  ( a e. ( G NeighbVtx b ) <-> ( ( a e. V /\ b e. V ) /\ a =/= b /\ E. e e. E { b , a } C_ e ) )
35 24 25 33 34 syl3anbrc
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> a e. ( G NeighbVtx b ) )
36 23 35 jca
 |-  ( ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) )
37 36 ex
 |-  ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) -> ( { a , b } e. E -> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) ) )
38 1 2 nbuhgr2vtx1edgblem
 |-  ( ( G e. UHGraph /\ V = { a , b } /\ a e. ( G NeighbVtx b ) ) -> { a , b } e. E )
39 38 3exp
 |-  ( G e. UHGraph -> ( V = { a , b } -> ( a e. ( G NeighbVtx b ) -> { a , b } e. E ) ) )
40 39 adantr
 |-  ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) -> ( V = { a , b } -> ( a e. ( G NeighbVtx b ) -> { a , b } e. E ) ) )
41 40 adantld
 |-  ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) -> ( ( a =/= b /\ V = { a , b } ) -> ( a e. ( G NeighbVtx b ) -> { a , b } e. E ) ) )
42 41 imp
 |-  ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) -> ( a e. ( G NeighbVtx b ) -> { a , b } e. E ) )
43 42 adantld
 |-  ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) -> ( ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) -> { a , b } e. E ) )
44 37 43 impbid
 |-  ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) -> ( { a , b } e. E <-> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) ) )
45 eleq1
 |-  ( V = { a , b } -> ( V e. E <-> { a , b } e. E ) )
46 45 adantl
 |-  ( ( a =/= b /\ V = { a , b } ) -> ( V e. E <-> { a , b } e. 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 } -> ( A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. ( { a , b } \ { v } ) n e. ( G NeighbVtx v ) ) )
50 47 49 raleqbidv
 |-  ( V = { a , b } -> ( A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> A. v e. { a , b } A. n e. ( { a , b } \ { v } ) n e. ( G NeighbVtx v ) ) )
51 vex
 |-  a e. _V
52 vex
 |-  b e. _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 e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx a ) ) )
57 54 56 raleqbidv
 |-  ( v = a -> ( A. n e. ( { a , b } \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. ( { a , b } \ { a } ) n e. ( 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 e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx b ) ) )
62 59 61 raleqbidv
 |-  ( v = b -> ( A. n e. ( { a , b } \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) )
63 51 52 57 62 ralpr
 |-  ( A. v e. { a , b } A. n e. ( { a , b } \ { v } ) n e. ( G NeighbVtx v ) <-> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) /\ A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) )
64 difprsn1
 |-  ( a =/= b -> ( { a , b } \ { a } ) = { b } )
65 64 raleqdv
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) <-> A. n e. { b } n e. ( G NeighbVtx a ) ) )
66 eleq1
 |-  ( n = b -> ( n e. ( G NeighbVtx a ) <-> b e. ( G NeighbVtx a ) ) )
67 52 66 ralsn
 |-  ( A. n e. { b } n e. ( G NeighbVtx a ) <-> b e. ( G NeighbVtx a ) )
68 65 67 bitrdi
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) <-> b e. ( G NeighbVtx a ) ) )
69 difprsn2
 |-  ( a =/= b -> ( { a , b } \ { b } ) = { a } )
70 69 raleqdv
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) <-> A. n e. { a } n e. ( G NeighbVtx b ) ) )
71 eleq1
 |-  ( n = a -> ( n e. ( G NeighbVtx b ) <-> a e. ( G NeighbVtx b ) ) )
72 51 71 ralsn
 |-  ( A. n e. { a } n e. ( G NeighbVtx b ) <-> a e. ( G NeighbVtx b ) )
73 70 72 bitrdi
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) <-> a e. ( G NeighbVtx b ) ) )
74 68 73 anbi12d
 |-  ( a =/= b -> ( ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) /\ A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) <-> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) ) )
75 63 74 syl5bb
 |-  ( a =/= b -> ( A. v e. { a , b } A. n e. ( { a , b } \ { v } ) n e. ( G NeighbVtx v ) <-> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) ) )
76 50 75 sylan9bbr
 |-  ( ( a =/= b /\ V = { a , b } ) -> ( A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) ) )
77 46 76 bibi12d
 |-  ( ( a =/= b /\ V = { a , b } ) -> ( ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) <-> ( { a , b } e. E <-> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) ) ) )
78 77 adantl
 |-  ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) -> ( ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) <-> ( { a , b } e. E <-> ( b e. ( G NeighbVtx a ) /\ a e. ( G NeighbVtx b ) ) ) ) )
79 44 78 mpbird
 |-  ( ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) /\ ( a =/= b /\ V = { a , b } ) ) -> ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
80 79 ex
 |-  ( ( G e. UHGraph /\ ( a e. V /\ b e. V ) ) -> ( ( a =/= b /\ V = { a , b } ) -> ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) ) )
81 80 rexlimdvva
 |-  ( G e. UHGraph -> ( E. a e. V E. b e. V ( a =/= b /\ V = { a , b } ) -> ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) ) )
82 5 81 syl5bi
 |-  ( G e. UHGraph -> ( ( # ` V ) = 2 -> ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) ) )
83 82 imp
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( V e. E <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )