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