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

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 
|- V = ( Vtx ` G )
nb3grpr.e 
|- E = ( Edg ` G )
nb3grpr.g 
|- ( ph -> G e. USGraph )
nb3grpr.t 
|- ( ph -> V = { A , B , C } )
nb3grpr.s 
|- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
nb3grpr.n 
|- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
Assertion nb3grpr 
|- ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )

Proof

Step Hyp Ref Expression
1 nb3grpr.v 
 |-  V = ( Vtx ` G )
2 nb3grpr.e 
 |-  E = ( Edg ` G )
3 nb3grpr.g 
 |-  ( ph -> G e. USGraph )
4 nb3grpr.t 
 |-  ( ph -> V = { A , B , C } )
5 nb3grpr.s 
 |-  ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
6 nb3grpr.n 
 |-  ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
7 id 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
8 prcom 
 |-  { A , B } = { B , A }
9 8 eleq1i 
 |-  ( { A , B } e. E <-> { B , A } e. E )
10 prcom 
 |-  { B , C } = { C , B }
11 10 eleq1i 
 |-  ( { B , C } e. E <-> { C , B } e. E )
12 prcom 
 |-  { C , A } = { A , C }
13 12 eleq1i 
 |-  ( { C , A } e. E <-> { A , C } e. E )
14 9 11 13 3anbi123i 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( { B , A } e. E /\ { C , B } e. E /\ { A , C } e. E ) )
15 3anrot 
 |-  ( ( { A , C } e. E /\ { B , A } e. E /\ { C , B } e. E ) <-> ( { B , A } e. E /\ { C , B } e. E /\ { A , C } e. E ) )
16 14 15 bitr4i 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( { A , C } e. E /\ { B , A } e. E /\ { C , B } e. E ) )
17 16 a1i 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( { A , C } e. E /\ { B , A } e. E /\ { C , B } e. E ) ) )
18 7 17 biadanii 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , A } e. E /\ { C , B } e. E ) ) )
19 an6 
 |-  ( ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , C } e. E /\ { B , A } e. E /\ { C , B } e. E ) ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , C } e. E /\ { B , A } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) )
20 18 19 bitri 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , C } e. E /\ { B , A } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) )
21 20 a1i 
 |-  ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , C } e. E /\ { B , A } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) ) )
22 1 2 3 4 5 nb3grprlem1 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( { A , B } e. E /\ { A , C } e. E ) ) )
23 tprot 
 |-  { A , B , C } = { B , C , A }
24 4 23 eqtrdi 
 |-  ( ph -> V = { B , C , A } )
25 3anrot 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ C e. Z /\ A e. X ) )
26 5 25 sylib 
 |-  ( ph -> ( B e. Y /\ C e. Z /\ A e. X ) )
27 1 2 3 24 26 nb3grprlem1 
 |-  ( ph -> ( ( G NeighbVtx B ) = { C , A } <-> ( { B , C } e. E /\ { B , A } e. E ) ) )
28 tprot 
 |-  { C , A , B } = { A , B , C }
29 4 28 eqtr4di 
 |-  ( ph -> V = { C , A , B } )
30 3anrot 
 |-  ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
31 5 30 sylibr 
 |-  ( ph -> ( C e. Z /\ A e. X /\ B e. Y ) )
32 1 2 3 29 31 nb3grprlem1 
 |-  ( ph -> ( ( G NeighbVtx C ) = { A , B } <-> ( { C , A } e. E /\ { C , B } e. E ) ) )
33 22 27 32 3anbi123d 
 |-  ( ph -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { C , A } /\ ( G NeighbVtx C ) = { A , B } ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { B , C } e. E /\ { B , A } e. E ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) ) )
34 1 2 3 4 5 6 nb3grprlem2 
 |-  ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx A ) = { y , z } ) )
35 necom 
 |-  ( A =/= B <-> B =/= A )
36 necom 
 |-  ( A =/= C <-> C =/= A )
37 biid 
 |-  ( B =/= C <-> B =/= C )
38 35 36 37 3anbi123i 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= A /\ C =/= A /\ B =/= C ) )
39 3anrot 
 |-  ( ( B =/= C /\ B =/= A /\ C =/= A ) <-> ( B =/= A /\ C =/= A /\ B =/= C ) )
40 38 39 bitr4i 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
41 6 40 sylib 
 |-  ( ph -> ( B =/= C /\ B =/= A /\ C =/= A ) )
42 1 2 3 24 26 41 nb3grprlem2 
 |-  ( ph -> ( ( G NeighbVtx B ) = { C , A } <-> E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx B ) = { y , z } ) )
43 3anrot 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ B =/= C /\ A =/= B ) )
44 necom 
 |-  ( B =/= C <-> C =/= B )
45 biid 
 |-  ( A =/= B <-> A =/= B )
46 36 44 45 3anbi123i 
 |-  ( ( A =/= C /\ B =/= C /\ A =/= B ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
47 43 46 bitri 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
48 6 47 sylib 
 |-  ( ph -> ( C =/= A /\ C =/= B /\ A =/= B ) )
49 1 2 3 29 31 48 nb3grprlem2 
 |-  ( ph -> ( ( G NeighbVtx C ) = { A , B } <-> E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx C ) = { y , z } ) )
50 34 42 49 3anbi123d 
 |-  ( ph -> ( ( ( G NeighbVtx A ) = { B , C } /\ ( G NeighbVtx B ) = { C , A } /\ ( G NeighbVtx C ) = { A , B } ) <-> ( E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx A ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx B ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx C ) = { y , z } ) ) )
51 21 33 50 3bitr2d 
 |-  ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx A ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx B ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx C ) = { y , z } ) ) )
52 oveq2 
 |-  ( x = A -> ( G NeighbVtx x ) = ( G NeighbVtx A ) )
53 52 eqeq1d 
 |-  ( x = A -> ( ( G NeighbVtx x ) = { y , z } <-> ( G NeighbVtx A ) = { y , z } ) )
54 53 2rexbidv 
 |-  ( x = A -> ( E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx A ) = { y , z } ) )
55 oveq2 
 |-  ( x = B -> ( G NeighbVtx x ) = ( G NeighbVtx B ) )
56 55 eqeq1d 
 |-  ( x = B -> ( ( G NeighbVtx x ) = { y , z } <-> ( G NeighbVtx B ) = { y , z } ) )
57 56 2rexbidv 
 |-  ( x = B -> ( E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx B ) = { y , z } ) )
58 oveq2 
 |-  ( x = C -> ( G NeighbVtx x ) = ( G NeighbVtx C ) )
59 58 eqeq1d 
 |-  ( x = C -> ( ( G NeighbVtx x ) = { y , z } <-> ( G NeighbVtx C ) = { y , z } ) )
60 59 2rexbidv 
 |-  ( x = C -> ( E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx C ) = { y , z } ) )
61 54 57 60 raltpg 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. x e. { A , B , C } E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> ( E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx A ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx B ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx C ) = { y , z } ) ) )
62 5 61 syl 
 |-  ( ph -> ( A. x e. { A , B , C } E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> ( E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx A ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx B ) = { y , z } /\ E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx C ) = { y , z } ) ) )
63 raleq 
 |-  ( V = { A , B , C } -> ( A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> A. x e. { A , B , C } E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )
64 63 bicomd 
 |-  ( V = { A , B , C } -> ( A. x e. { A , B , C } E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )
65 4 64 syl 
 |-  ( ph -> ( A. x e. { A , B , C } E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )
66 51 62 65 3bitr2d 
 |-  ( ph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> A. x e. V E. y e. V E. z e. ( V \ { y } ) ( G NeighbVtx x ) = { y , z } ) )