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

Metamath Proof Explorer

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 𝐶 ) = { 𝐴 , 𝐵 } ) ) )