Metamath Proof Explorer

Theorem nb3grpr2

Description: The neighbors of a vertex in a simple graph with three elements are an unordered pair of the other vertices iff all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Hypotheses nb3grpr.v 
|- V = ( Vtx ` G )
nb3grpr.e 
|- E = ( Edg ` G )
nb3grpr.g 
|- ( ph -> G e. USGraph )
nb3grpr.t 
|- ( ph -> V = { A , B , C } )
nb3grpr.s 
|- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
nb3grpr.n 
|- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
Assertion nb3grpr2 
|- ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) ) )

Proof

Step Hyp Ref Expression
1 nb3grpr.v 
 |-  V = ( Vtx ` G )
2 nb3grpr.e 
 |-  E = ( Edg ` G )
3 nb3grpr.g 
 |-  ( ph -> G e. USGraph )
4 nb3grpr.t 
 |-  ( ph -> V = { A , B , C } )
5 nb3grpr.s 
 |-  ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
6 nb3grpr.n 
 |-  ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
7 3anan32 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { C , A } e. E ) /\ { B , C } e. E ) )
8 7 a1i 
 |-  ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { C , A } e. E ) /\ { B , C } e. E ) ) )
9 prcom 
 |-  { C , A } = { A , C }
10 9 eleq1i 
 |-  ( { C , A } e. E <-> { A , C } e. E )
11 10 biimpi 
 |-  ( { C , A } e. E -> { A , C } e. E )
12 11 pm4.71i 
 |-  ( { C , A } e. E <-> ( { C , A } e. E /\ { A , C } e. E ) )
13 12 bianass 
 |-  ( ( { A , B } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { C , A } e. E ) /\ { A , C } e. E ) )
14 13 anbi1i 
 |-  ( ( ( { A , B } e. E /\ { C , A } e. E ) /\ { B , C } e. E ) <-> ( ( ( { A , B } e. E /\ { C , A } e. E ) /\ { A , C } e. E ) /\ { B , C } e. E ) )
15 anass 
 |-  ( ( ( ( { A , B } e. E /\ { C , A } e. E ) /\ { A , C } e. E ) /\ { B , C } e. E ) <-> ( ( { A , B } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , C } e. E ) ) )
16 14 15 bitri 
 |-  ( ( ( { A , B } e. E /\ { C , A } e. E ) /\ { B , C } e. E ) <-> ( ( { A , B } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , C } e. E ) ) )
17 8 16 bitrdi 
 |-  ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , C } e. E ) ) ) )
18 prcom 
 |-  { A , B } = { B , A }
19 18 eleq1i 
 |-  ( { A , B } e. E <-> { B , A } e. E )
20 19 biimpi 
 |-  ( { A , B } e. E -> { B , A } e. E )
21 20 pm4.71i 
 |-  ( { A , B } e. E <-> ( { A , B } e. E /\ { B , A } e. E ) )
22 21 anbi1i 
 |-  ( ( { A , B } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { B , A } e. E ) /\ { C , A } e. E ) )
23 df-3an 
 |-  ( ( { A , B } e. E /\ { B , A } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { B , A } e. E ) /\ { C , A } e. E ) )
24 22 23 bitr4i 
 |-  ( ( { A , B } e. E /\ { C , A } e. E ) <-> ( { A , B } e. E /\ { B , A } e. E /\ { C , A } e. E ) )
25 prcom 
 |-  { B , C } = { C , B }
26 25 eleq1i 
 |-  ( { B , C } e. E <-> { C , B } e. E )
27 26 biimpi 
 |-  ( { B , C } e. E -> { C , B } e. E )
28 27 pm4.71i 
 |-  ( { B , C } e. E <-> ( { B , C } e. E /\ { C , B } e. E ) )
29 28 anbi2i 
 |-  ( ( { A , C } e. E /\ { B , C } e. E ) <-> ( { A , C } e. E /\ ( { B , C } e. E /\ { C , B } e. E ) ) )
30 3anass 
 |-  ( ( { A , C } e. E /\ { B , C } e. E /\ { C , B } e. E ) <-> ( { A , C } e. E /\ ( { B , C } e. E /\ { C , B } e. E ) ) )
31 29 30 bitr4i 
 |-  ( ( { A , C } e. E /\ { B , C } e. E ) <-> ( { A , C } e. E /\ { B , C } e. E /\ { C , B } e. E ) )
32 24 31 anbi12i 
 |-  ( ( ( { A , B } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , C } e. E ) ) <-> ( ( { A , B } e. E /\ { B , A } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , C } e. E /\ { C , B } e. E ) ) )
33 an6 
 |-  ( ( ( { A , B } e. E /\ { B , A } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , C } e. E /\ { C , B } e. E ) ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) )
34 32 33 bitri 
 |-  ( ( ( { A , B } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , C } e. E ) ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) )
35 17 34 bitrdi 
 |-  ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) ) )
36 1 2 3 4 5 nb3grprlem1 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( { A , B } e. E /\ { A , C } e. E ) ) )
37 tpcoma 
 |-  { A , B , C } = { B , A , C }
38 4 37 eqtrdi 
 |-  ( ph -> V = { B , A , C } )
39 3ancoma 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
40 5 39 sylib 
 |-  ( ph -> ( B e. Y /\ A e. X /\ C e. Z ) )
41 1 2 3 38 40 nb3grprlem1 
 |-  ( ph -> ( ( G NeighbVtx B ) = { A , C } <-> ( { B , A } e. E /\ { B , C } e. E ) ) )
42 tprot 
 |-  { C , A , B } = { A , B , C }
43 4 42 eqtr4di 
 |-  ( ph -> V = { C , A , B } )
44 3anrot 
 |-  ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
45 5 44 sylibr 
 |-  ( ph -> ( C e. Z /\ A e. X /\ B e. Y ) )
46 1 2 3 43 45 nb3grprlem1 
 |-  ( ph -> ( ( G NeighbVtx C ) = { A , B } <-> ( { C , A } e. E /\ { C , B } e. E ) ) )
47 36 41 46 3anbi123d 
 |-  ( ph -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) ) )
48 35 47 bitr4d 
 |-  ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) ) )