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 biimpi 
 |-  ( { A , C } e. ( Edg ` G ) -> { C , A } e. ( Edg ` G ) )
4 3 adantl 
 |-  ( ( { A , B } e. ( Edg ` G ) /\ { A , C } e. ( Edg ` G ) ) -> { C , A } e. ( Edg ` G ) )
5 prcom 
 |-  { B , C } = { C , B }
6 5 eleq1i 
 |-  ( { B , C } e. ( Edg ` G ) <-> { C , B } e. ( Edg ` G ) )
7 6 biimpi 
 |-  ( { B , C } e. ( Edg ` G ) -> { C , B } e. ( Edg ` G ) )
8 7 adantl 
 |-  ( ( { B , A } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) -> { C , B } e. ( Edg ` G ) )
9 4 8 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 ) ) )
10 9 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 ) ) ) )
11 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
12 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
13 simprr 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> G e. USGraph )
14 simprl 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) ) -> ( Vtx ` G ) = { A , B , C } )
15 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 ) )
16 11 12 13 14 15 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 ) ) ) )
17 3ancoma 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
18 17 biimpi 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( B e. Y /\ A e. X /\ C e. Z ) )
19 tpcoma 
 |-  { A , B , C } = { B , A , C }
20 19 eqeq2i 
 |-  ( ( Vtx ` G ) = { A , B , C } <-> ( Vtx ` G ) = { B , A , C } )
21 20 biimpi 
 |-  ( ( Vtx ` G ) = { A , B , C } -> ( Vtx ` G ) = { B , A , C } )
22 21 anim1i 
 |-  ( ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) -> ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) )
23 simprr 
 |-  ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) ) -> G e. USGraph )
24 simprl 
 |-  ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( ( Vtx ` G ) = { B , A , C } /\ G e. USGraph ) ) -> ( Vtx ` G ) = { B , A , C } )
25 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 ) )
26 11 12 23 24 25 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 ) ) ) )
27 18 22 26 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 ) ) ) )
28 16 27 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 ) ) ) ) )
29 3anrot 
 |-  ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
30 29 biimpri 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
31 tprot 
 |-  { C , A , B } = { A , B , C }
32 31 eqcomi 
 |-  { A , B , C } = { C , A , B }
33 32 eqeq2i 
 |-  ( ( Vtx ` G ) = { A , B , C } <-> ( Vtx ` G ) = { C , A , B } )
34 33 anbi1i 
 |-  ( ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) <-> ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) )
35 34 biimpi 
 |-  ( ( ( Vtx ` G ) = { A , B , C } /\ G e. USGraph ) -> ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) )
36 simprr 
 |-  ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) ) -> G e. USGraph )
37 simprl 
 |-  ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( ( Vtx ` G ) = { C , A , B } /\ G e. USGraph ) ) -> ( Vtx ` G ) = { C , A , B } )
38 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 ) )
39 11 12 36 37 38 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 ) ) ) )
40 30 35 39 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 ) ) ) )
41 10 28 40 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 } ) )
42 41 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 } ) ) )
43 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 } ) )
44 42 43 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 } ) ) )