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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	nb3grpr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	nb3grpr.g	⊢ ( 𝜑 → 𝐺 ∈ USGraph )
	nb3grpr.t	⊢ ( 𝜑 → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
	nb3grpr.s	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
	nb3grpr.n	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
Assertion	nb3grpr2	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		nb3grpr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nb3grpr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		nb3grpr.g	⊢ ( 𝜑 → 𝐺 ∈ USGraph )
4		nb3grpr.t	⊢ ( 𝜑 → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
5		nb3grpr.s	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
6		nb3grpr.n	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
7		3anan32	⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
8	7	a1i	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
9		prcom	⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
10	9	eleq1i	⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ { 𝐴 , 𝐶 } ∈ 𝐸 )
11	10	biimpi	⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 → { 𝐴 , 𝐶 } ∈ 𝐸 )
12	11	pm4.71i	⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
13	12	bianass	⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
14	13	anbi1i	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
15		anass	⊢ ( ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
16	14 15	bitri	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
17	8 16	bitrdi	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ) )
18		prcom	⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
19	18	eleq1i	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐵 , 𝐴 } ∈ 𝐸 )
20	19	biimpi	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 → { 𝐵 , 𝐴 } ∈ 𝐸 )
21	20	pm4.71i	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) )
22	21	anbi1i	⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
23		df-3an	⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
24	22 23	bitr4i	⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
25		prcom	⊢ { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 }
26	25	eleq1i	⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐶 , 𝐵 } ∈ 𝐸 )
27	26	biimpi	⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 → { 𝐶 , 𝐵 } ∈ 𝐸 )
28	27	pm4.71i	⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
29	28	anbi2i	⊢ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
30		3anass	⊢ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
31	29 30	bitr4i	⊢ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
32	24 31	anbi12i	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
33		an6	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
34	32 33	bitri	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
35	17 34	bitrdi	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
36	1 2 3 4 5	nb3grprlem1	⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )
37		tpcoma	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐴 , 𝐶 }
38	4 37	eqtrdi	⊢ ( 𝜑 → 𝑉 = { 𝐵 , 𝐴 , 𝐶 } )
39		3ancoma	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ↔ ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) )
40	5 39	sylib	⊢ ( 𝜑 → ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) )
41	1 2 3 38 40	nb3grprlem1	⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
42		tprot	⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
43	4 42	eqtr4di	⊢ ( 𝜑 → 𝑉 = { 𝐶 , 𝐴 , 𝐵 } )
44		3anrot	⊢ ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
45	5 44	sylibr	⊢ ( 𝜑 → ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
46	1 2 3 43 45	nb3grprlem1	⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
47	36 41 46	3anbi123d	⊢ ( 𝜑 → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
48	35 47	bitr4d	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐴 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ) )