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