Metamath Proof Explorer

Theorem nbgr2vtx1edg

Description: If a graph 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) (Revised by AV, 25-Mar-2021) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbgr2vtx1edg.v 
|- V = ( Vtx ` G )
nbgr2vtx1edg.e 
|- E = ( Edg ` G )
Assertion nbgr2vtx1edg 
|- ( ( ( # ` 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 simpll 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> ( a e. V /\ b e. V ) )
7 6 ancomd 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> ( b e. V /\ a e. V ) )
8 simpl 
 |-  ( ( a =/= b /\ V = { a , b } ) -> a =/= b )
9 8 necomd 
 |-  ( ( a =/= b /\ V = { a , b } ) -> b =/= a )
10 9 ad2antlr 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> b =/= a )
11 id 
 |-  ( { a , b } e. E -> { a , b } e. E )
12 sseq2 
 |-  ( e = { a , b } -> ( { a , b } C_ e <-> { a , b } C_ { a , b } ) )
13 12 adantl 
 |-  ( ( { a , b } e. E /\ e = { a , b } ) -> ( { a , b } C_ e <-> { a , b } C_ { a , b } ) )
14 ssidd 
 |-  ( { a , b } e. E -> { a , b } C_ { a , b } )
15 11 13 14 rspcedvd 
 |-  ( { a , b } e. E -> E. e e. E { a , b } C_ e )
16 15 adantl 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> E. e e. E { a , b } C_ e )
17 1 2 nbgrel 
 |-  ( b e. ( G NeighbVtx a ) <-> ( ( b e. V /\ a e. V ) /\ b =/= a /\ E. e e. E { a , b } C_ e ) )
18 7 10 16 17 syl3anbrc 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> b e. ( G NeighbVtx a ) )
19 8 ad2antlr 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> a =/= b )
20 sseq2 
 |-  ( e = { a , b } -> ( { b , a } C_ e <-> { b , a } C_ { a , b } ) )
21 20 adantl 
 |-  ( ( { a , b } e. E /\ e = { a , b } ) -> ( { b , a } C_ e <-> { b , a } C_ { a , b } ) )
22 prcom 
 |-  { b , a } = { a , b }
23 22 eqimssi 
 |-  { b , a } C_ { a , b }
24 23 a1i 
 |-  ( { a , b } e. E -> { b , a } C_ { a , b } )
25 11 21 24 rspcedvd 
 |-  ( { a , b } e. E -> E. e e. E { b , a } C_ e )
26 25 adantl 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> E. e e. E { b , a } C_ e )
27 1 2 nbgrel 
 |-  ( a e. ( G NeighbVtx b ) <-> ( ( a e. V /\ b e. V ) /\ a =/= b /\ E. e e. E { b , a } C_ e ) )
28 6 19 26 27 syl3anbrc 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> a e. ( G NeighbVtx b ) )
29 difprsn1 
 |-  ( a =/= b -> ( { a , b } \ { a } ) = { b } )
30 29 raleqdv 
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) <-> A. n e. { b } n e. ( G NeighbVtx a ) ) )
31 vex 
 |-  b e. _V
32 eleq1 
 |-  ( n = b -> ( n e. ( G NeighbVtx a ) <-> b e. ( G NeighbVtx a ) ) )
33 31 32 ralsn 
 |-  ( A. n e. { b } n e. ( G NeighbVtx a ) <-> b e. ( G NeighbVtx a ) )
34 30 33 bitrdi 
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) <-> b e. ( G NeighbVtx a ) ) )
35 difprsn2 
 |-  ( a =/= b -> ( { a , b } \ { b } ) = { a } )
36 35 raleqdv 
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) <-> A. n e. { a } n e. ( G NeighbVtx b ) ) )
37 vex 
 |-  a e. _V
38 eleq1 
 |-  ( n = a -> ( n e. ( G NeighbVtx b ) <-> a e. ( G NeighbVtx b ) ) )
39 37 38 ralsn 
 |-  ( A. n e. { a } n e. ( G NeighbVtx b ) <-> a e. ( G NeighbVtx b ) )
40 36 39 bitrdi 
 |-  ( a =/= b -> ( A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) <-> a e. ( G NeighbVtx b ) ) )
41 34 40 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 ) ) ) )
42 41 adantr 
 |-  ( ( a =/= b /\ V = { 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 ) ) ) )
43 42 ad2antlr 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> ( ( 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 ) ) ) )
44 18 28 43 mpbir2and 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) /\ { a , b } e. E ) -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) /\ A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) )
45 44 ex 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) -> ( { a , b } e. E -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) /\ A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) ) )
46 eleq1 
 |-  ( 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 sneq 
 |-  ( v = a -> { v } = { a } )
52 51 difeq2d 
 |-  ( v = a -> ( { a , b } \ { v } ) = ( { a , b } \ { a } ) )
53 oveq2 
 |-  ( v = a -> ( G NeighbVtx v ) = ( G NeighbVtx a ) )
54 53 eleq2d 
 |-  ( v = a -> ( n e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx a ) ) )
55 52 54 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 ) ) )
56 sneq 
 |-  ( v = b -> { v } = { b } )
57 56 difeq2d 
 |-  ( v = b -> ( { a , b } \ { v } ) = ( { a , b } \ { b } ) )
58 oveq2 
 |-  ( v = b -> ( G NeighbVtx v ) = ( G NeighbVtx b ) )
59 58 eleq2d 
 |-  ( v = b -> ( n e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx b ) ) )
60 57 59 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 ) ) )
61 37 31 55 60 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 ) ) )
62 50 61 bitrdi 
 |-  ( V = { a , b } -> ( A. v e. V A. n e. ( V \ { 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 ) ) ) )
63 46 62 imbi12d 
 |-  ( V = { a , b } -> ( ( V e. E -> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) <-> ( { a , b } e. E -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) /\ A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) ) ) )
64 63 adantl 
 |-  ( ( 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 -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) /\ A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) ) ) )
65 64 adantl 
 |-  ( ( ( 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 -> ( A. n e. ( { a , b } \ { a } ) n e. ( G NeighbVtx a ) /\ A. n e. ( { a , b } \ { b } ) n e. ( G NeighbVtx b ) ) ) ) )
66 45 65 mpbird 
 |-  ( ( ( 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 ) ) )
67 66 ex 
 |-  ( ( 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 ) ) ) )
68 67 rexlimivv 
 |-  ( 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 ) ) )
69 5 68 sylbi 
 |-  ( ( # ` V ) = 2 -> ( V e. E -> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
70 69 imp 
 |-  ( ( ( # ` V ) = 2 /\ V e. E ) -> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) )