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 ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ) ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ) )

Proof

Step Hyp Ref Expression
1 prcom ⊢ { 𝐴 , 𝐶 } = { 𝐶 , 𝐴 }
2 1 eleq1i ⊢ ( { 𝐴 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) )
3 2 bilani ⊢ ( ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐴 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) → { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) )
4 prcom ⊢ { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 }
5 4 eleq1i ⊢ ( { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
6 5 bilani ⊢ ( ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) → { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
7 3 6 anim12i ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐴 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) )
8 7 a1i ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐴 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
9 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
11 simprr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐺 ∈ USGraph )
12 simprl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } )
13 simpl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
14 9 10 11 12 13 nb3grprlem1 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐴 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) )
15 3ancoma ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ↔ ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) )
16 15 biimpi ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) )
17 tpcoma ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐴 , 𝐶 }
18 17 eqeq2i ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ↔ ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } )
19 18 biimpi ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } → ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } )
20 19 anim1i ⊢ ( ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) )
21 simprr ⊢ ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐺 ∈ USGraph )
22 simprl ⊢ ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } )
23 simpl ⊢ ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) )
24 9 10 21 22 23 nb3grprlem1 ⊢ ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ↔ ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) )
25 16 20 24 syl2an ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ↔ ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) )
26 14 25 anbi12d ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ) ↔ ( ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐴 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
27 3anrot ⊢ ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
28 27 biimpri ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
29 tprot ⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
30 29 eqcomi ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 , 𝐵 }
31 30 eqeq2i ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ↔ ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } )
32 31 anbi1i ⊢ ( ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ↔ ( ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) )
33 32 biimpi ⊢ ( ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) )
34 simprr ⊢ ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → 𝐺 ∈ USGraph )
35 simprl ⊢ ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } )
36 simpl ⊢ ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
37 9 10 34 35 36 nb3grprlem1 ⊢ ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ↔ ( { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
38 28 33 37 syl2an ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ↔ ( { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
39 8 26 38 3imtr4d ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ) → ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) )
40 39 pm4.71d ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ) ↔ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ) ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ) )
41 df-3an ⊢ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ↔ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ) ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) )
42 40 41 bitr4di ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ) ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ) )