Theorem cusgr3vnbpr

Description: The neighbors of a vertex in a simple graph with three elements are unordered pairs of the other vertices if and only if the graph is complete. (Contributed by Alexander van der Vekens, 18-Oct-2017) (Revised by AV, 5-Nov-2020)

	Ref	Expression
Hypotheses	cplgr3v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	cplgr3v.t	⊢ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 }
	cplgr3v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	cusgr3vnbpr	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ) )

Proof

Step	Hyp	Ref	Expression
1		cplgr3v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		cplgr3v.t	⊢ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 , 𝐶 }
3		cplgr3v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		usgrupgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
5	1 2	cplgr3v	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ UPGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐺 ∈ ComplGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
6	4 5	syl3an2	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐺 ∈ ComplGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
7		simp2	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → 𝐺 ∈ USGraph )
8	3 2	eqtri	⊢ 𝑉 = { 𝐴 , 𝐵 , 𝐶 }
9	8	a1i	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
10		simp1	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
11		simp3	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
12	3 1 7 9 10 11	nb3grpr	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ) )
13	6 12	bitrd	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝐺 ∈ USGraph ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ) )