This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nb3gr2nb

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

Ref Expression
Assertion nb3gr2nb 
|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) <-> ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) ) )

Proof

Step Hyp Ref Expression
1 prcom 
 |-  { A , C } = { C , A }
2 1 eleq1i 
 |-  ( { A , C } e. ( Edg ` G ) <-> { C , A } e. ( Edg ` G ) )
3 2 bilani 
 |-  ( ( { A , B } e. ( Edg ` G ) /\ { A , C } e. ( Edg ` G ) ) -> { C , A } e. ( Edg ` G ) )
4 prcom 
 |-  { B , C } = { C , B }
5 4 eleq1i 
 |-  ( { B , C } e. ( Edg ` G ) <-> { C , B } e. ( Edg ` G ) )
6 5 bilani 
 |-  ( ( { B , A } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) -> { C , B } e. ( Edg ` G ) )
7 3 6 anim12i 
 |-  ( ( ( { A , B } e. ( Edg ` G ) /\ { A , C } e. ( Edg ` G ) ) /\ ( { B , A } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) ) -> ( { C , A } e. ( Edg ` G ) /\ { C , B } e. ( Edg ` G ) ) )
8 7 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( { A , B } e. ( Edg ` G ) /\ { A , C } e. ( Edg ` G ) ) /\ ( { B , A } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) ) -> ( { C , A } e. ( Edg ` G ) /\ { C , B } e. ( Edg ` G ) ) ) )
9 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
10 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
11 simprr 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> G e. USGraph )
12 simprl 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( Vtx ` G ) = { A , B , C } )
13 simpl 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( A e. X /\ B e. Y /\ C e. Z ) )
14 9 10 11 12 13 nb3grprlem1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( G NeighbVtx A ) = { B , C } <-> ( { A , B } e. ( Edg ` G ) /\ { A , C } e. ( Edg ` G ) ) ) )
15 3ancoma 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
16 15 biimpi 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( B e. Y /\ A e. X /\ C e. Z ) )
17 tpcoma 
 |-  { A , B , C } = { B , A , C }
18 17 eqeq2i 
 |-  ( ( Vtx ` G ) = { A , B , C } <-> ( Vtx ` G ) = { B , A , C } )
19 18 biimpi 
 |-  ( ( Vtx ` G ) = { A , B , C } -> ( Vtx ` G ) = { B , A , C } )
20 19 anim1i 
 |-  ( ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) -> ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) )
21 simprr 
 |-  ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) ) -> G e. USGraph )
22 simprl 
 |-  ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) ) -> ( Vtx ` G ) = { B , A , C } )
23 simpl 
 |-  ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) ) -> ( B e. Y /\ A e. X /\ C e. Z ) )
24 9 10 21 22 23 nb3grprlem1 
 |-  ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) ) -> ( ( G NeighbVtx B ) = { A , C } <-> ( { B , A } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) ) )
25 16 20 24 syl2an 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( G NeighbVtx B ) = { A , C } <-> ( { B , A } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) ) )
26 14 25 anbi12d 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) <-> ( ( { A , B } e. ( Edg ` G ) /\ { A , C } e. ( Edg ` G ) ) /\ ( { B , A } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) ) ) )
27 3anrot 
 |-  ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
28 27 biimpri 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
29 tprot 
 |-  { C , A , B } = { A , B , C }
30 29 eqcomi 
 |-  { A , B , C } = { C , A , B }
31 30 eqeq2i 
 |-  ( ( Vtx ` G ) = { A , B , C } <-> ( Vtx ` G ) = { C , A , B } )
32 31 anbi1i 
 |-  ( ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) <-> ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) )
33 32 biimpi 
 |-  ( ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) -> ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) )
34 simprr 
 |-  ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) ) -> G e. USGraph )
35 simprl 
 |-  ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) ) -> ( Vtx ` G ) = { C , A , B } )
36 simpl 
 |-  ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
37 9 10 34 35 36 nb3grprlem1 
 |-  ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) ) -> ( ( G NeighbVtx C ) = { A , B } <-> ( { C , A } e. ( Edg ` G ) /\ { C , B } e. ( Edg ` G ) ) ) )
38 28 33 37 syl2an 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( G NeighbVtx C ) = { A , B } <-> ( { C , A } e. ( Edg ` G ) /\ { C , B } e. ( Edg ` G ) ) ) )
39 8 26 38 3imtr4d 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) -> ( G NeighbVtx C ) = { A , B } ) )
40 39 pm4.71d 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) <-> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) /\ ( G NeighbVtx C ) = { A , B } ) ) )
41 df-3an 
 |-  ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) <-> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) /\ ( G NeighbVtx C ) = { A , B } ) )
42 40 41 bitr4di 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } ) <-> ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { A , C } /\ ( G NeighbVtx C ) = { A , B } ) ) )