Metamath Proof Explorer

Theorem cusgr3vnbpr

Description: The neighbors of a vertex in a simple graph with three elements are unordered pairs of the other vertices if and only if the graph is complete. (Contributed by Alexander van der Vekens, 18-Oct-2017) (Revised by AV, 5-Nov-2020)

Ref Expression
Hypotheses cplgr3v.e 
|- E = ( Edg ` G )
cplgr3v.t 
|- ( Vtx ` G ) = { A , B , C }
cplgr3v.v 
|- V = ( Vtx ` G )
Assertion cusgr3vnbpr 
|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )

Proof

Step Hyp Ref Expression
1 cplgr3v.e 
 |-  E = ( Edg ` G )
2 cplgr3v.t 
 |-  ( Vtx ` G ) = { A , B , C }
3 cplgr3v.v 
 |-  V = ( Vtx ` G )
4 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
5 1 2 cplgr3v 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. UPGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
6 4 5 syl3an2 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
7 simp2 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> G e. USGraph )
8 3 2 eqtri 
 |-  V = { A , B , C }
9 8 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> V = { A , B , C } )
10 simp1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( A e. X /\ B e. Y /\ C e. Z ) )
11 simp3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( A =/= B /\ A =/= C /\ B =/= C ) )
12 3 1 7 9 10 11 nb3grpr 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )
13 6 12 bitrd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ G e. USGraph /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( G e. ComplGraph <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )