This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 ) = { 𝑦 , 𝑧 } ) )