Metamath Proof Explorer

Theorem nb3grpr

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 nb3grpr ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 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 id ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
8 prcom ⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
9 8 eleq1i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐵 , 𝐴 } ∈ 𝐸 )
10 prcom ⊢ { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 }
11 10 eleq1i ⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐶 , 𝐵 } ∈ 𝐸 )
12 prcom ⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
13 12 eleq1i ⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ { 𝐴 , 𝐶 } ∈ 𝐸 )
14 9 11 13 3anbi123i ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
15 3anrot ⊢ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
16 14 15 bitr4i ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
17 16 a1i ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
18 7 17 biadanii ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
19 an6 ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
20 18 19 bitri ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
21 20 a1i ⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
22 1 2 3 4 5 nb3grprlem1 ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )
23 tprot ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
24 4 23 eqtrdi ⊢ ( 𝜑 → 𝑉 = { 𝐵 , 𝐶 , 𝐴 } )
25 3anrot ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ↔ ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) )
26 5 25 sylib ⊢ ( 𝜑 → ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) )
27 1 2 3 24 26 nb3grprlem1 ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐵 ) = { 𝐶 , 𝐴 } ↔ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) )
28 tprot ⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
29 4 28 eqtr4di ⊢ ( 𝜑 → 𝑉 = { 𝐶 , 𝐴 , 𝐵 } )
30 3anrot ⊢ ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
31 5 30 sylibr ⊢ ( 𝜑 → ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
32 1 2 3 29 31 nb3grprlem1 ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
33 22 27 32 3anbi123d ⊢ ( 𝜑 → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐶 , 𝐴 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
34 1 2 3 4 5 6 nb3grprlem2 ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑦 , 𝑧 } ) )
35 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
36 necom ⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
37 biid ⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶 )
38 35 36 37 3anbi123i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ↔ ( 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) )
39 3anrot ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) ↔ ( 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ) )
40 38 39 bitr4i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ↔ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) )
41 6 40 sylib ⊢ ( 𝜑 → ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) )
42 1 2 3 24 26 41 nb3grprlem2 ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐵 ) = { 𝐶 , 𝐴 } ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐵 ) = { 𝑦 , 𝑧 } ) )
43 3anrot ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ) )
44 necom ⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 )
45 biid ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐵 )
46 36 44 45 3anbi123i ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
47 43 46 bitri ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ↔ ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
48 6 47 sylib ⊢ ( 𝜑 → ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
49 1 2 3 29 31 48 nb3grprlem2 ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐶 ) = { 𝑦 , 𝑧 } ) )
50 34 42 49 3anbi123d ⊢ ( 𝜑 → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∧ ( 𝐺 NeighbVtx 𝐵 ) = { 𝐶 , 𝐴 } ∧ ( 𝐺 NeighbVtx 𝐶 ) = { 𝐴 , 𝐵 } ) ↔ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐵 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐶 ) = { 𝑦 , 𝑧 } ) ) )
51 21 33 50 3bitr2d ⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐵 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐶 ) = { 𝑦 , 𝑧 } ) ) )
52 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝐴 ) )
53 52 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝑦 , 𝑧 } ) )
54 53 2rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑦 , 𝑧 } ) )
55 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝐵 ) )
56 55 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ( 𝐺 NeighbVtx 𝐵 ) = { 𝑦 , 𝑧 } ) )
57 56 2rexbidv ⊢ ( 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐵 ) = { 𝑦 , 𝑧 } ) )
58 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝐶 ) )
59 58 eqeq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ( 𝐺 NeighbVtx 𝐶 ) = { 𝑦 , 𝑧 } ) )
60 59 2rexbidv ⊢ ( 𝑥 = 𝐶 → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐶 ) = { 𝑦 , 𝑧 } ) )
61 54 57 60 raltpg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐵 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐶 ) = { 𝑦 , 𝑧 } ) ) )
62 5 61 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐵 ) = { 𝑦 , 𝑧 } ∧ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝐶 ) = { 𝑦 , 𝑧 } ) ) )
63 raleq ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ) )
64 63 bicomd ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ) )
65 4 64 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ↔ ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ) )
66 51 62 65 3bitr2d ⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ∀ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ( 𝐺 NeighbVtx 𝑥 ) = { 𝑦 , 𝑧 } ) )