Metamath Proof Explorer

Theorem pgnbgreunbgr

Description: In a Petersen graph, two different neighbors of a vertex have exactly one common neighbor, which is the vertex itself. (Contributed by AV, 9-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g 
|- G = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v 
|- V = ( Vtx ` G )
pgnbgreunbgr.e 
|- E = ( Edg ` G )
pgnbgreunbgr.n 
|- N = ( G NeighbVtx X )
Assertion pgnbgreunbgr 
|- ( ( K e. N /\ L e. N /\ K =/= L ) -> E! x e. V { { K , x } , { x , L } } C_ E )

Proof

Step Hyp Ref Expression
1 pgnbgreunbgr.g 
 |-  G = ( 5 gPetersenGr 2 )
2 pgnbgreunbgr.v 
 |-  V = ( Vtx ` G )
3 pgnbgreunbgr.e 
 |-  E = ( Edg ` G )
4 pgnbgreunbgr.n 
 |-  N = ( G NeighbVtx X )
5 preq2 
 |-  ( x = X -> { K , x } = { K , X } )
6 preq1 
 |-  ( x = X -> { x , L } = { X , L } )
7 5 6 preq12d 
 |-  ( x = X -> { { K , x } , { x , L } } = { { K , X } , { X , L } } )
8 7 sseq1d 
 |-  ( x = X -> ( { { K , x } , { x , L } } C_ E <-> { { K , X } , { X , L } } C_ E ) )
9 eqeq1 
 |-  ( x = X -> ( x = y <-> X = y ) )
10 9 imbi2d 
 |-  ( x = X -> ( ( { { K , y } , { y , L } } C_ E -> x = y ) <-> ( { { K , y } , { y , L } } C_ E -> X = y ) ) )
11 10 ralbidv 
 |-  ( x = X -> ( A. y e. V ( { { K , y } , { y , L } } C_ E -> x = y ) <-> A. y e. V ( { { K , y } , { y , L } } C_ E -> X = y ) ) )
12 8 11 anbi12d 
 |-  ( x = X -> ( ( { { K , x } , { x , L } } C_ E /\ A. y e. V ( { { K , y } , { y , L } } C_ E -> x = y ) ) <-> ( { { K , X } , { X , L } } C_ E /\ A. y e. V ( { { K , y } , { y , L } } C_ E -> X = y ) ) ) )
13 4 eleq2i 
 |-  ( K e. N <-> K e. ( G NeighbVtx X ) )
14 13 biimpi 
 |-  ( K e. N -> K e. ( G NeighbVtx X ) )
15 14 3ad2ant1 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> K e. ( G NeighbVtx X ) )
16 pgjsgr 
 |-  ( 5 gPetersenGr 2 ) e. USGraph
17 1 16 eqeltri 
 |-  G e. USGraph
18 3 nbusgreledg 
 |-  ( G e. USGraph -> ( K e. ( G NeighbVtx X ) <-> { K , X } e. E ) )
19 17 18 ax-mp 
 |-  ( K e. ( G NeighbVtx X ) <-> { K , X } e. E )
20 15 19 sylib 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> { K , X } e. E )
21 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
22 17 21 ax-mp 
 |-  G e. UMGraph
23 20 22 jctil 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> ( G e. UMGraph /\ { K , X } e. E ) )
24 2 3 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { K , X } e. E ) -> ( K e. V /\ X e. V ) )
25 simpr 
 |-  ( ( K e. V /\ X e. V ) -> X e. V )
26 23 24 25 3syl 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> X e. V )
27 4 eleq2i 
 |-  ( L e. N <-> L e. ( G NeighbVtx X ) )
28 13 27 anbi12i 
 |-  ( ( K e. N /\ L e. N ) <-> ( K e. ( G NeighbVtx X ) /\ L e. ( G NeighbVtx X ) ) )
29 3 nbusgreledg 
 |-  ( G e. USGraph -> ( L e. ( G NeighbVtx X ) <-> { L , X } e. E ) )
30 prcom 
 |-  { L , X } = { X , L }
31 30 eleq1i 
 |-  ( { L , X } e. E <-> { X , L } e. E )
32 29 31 bitrdi 
 |-  ( G e. USGraph -> ( L e. ( G NeighbVtx X ) <-> { X , L } e. E ) )
33 18 32 anbi12d 
 |-  ( G e. USGraph -> ( ( K e. ( G NeighbVtx X ) /\ L e. ( G NeighbVtx X ) ) <-> ( { K , X } e. E /\ { X , L } e. E ) ) )
34 17 33 ax-mp 
 |-  ( ( K e. ( G NeighbVtx X ) /\ L e. ( G NeighbVtx X ) ) <-> ( { K , X } e. E /\ { X , L } e. E ) )
35 28 34 sylbb 
 |-  ( ( K e. N /\ L e. N ) -> ( { K , X } e. E /\ { X , L } e. E ) )
36 35 3adant3 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> ( { K , X } e. E /\ { X , L } e. E ) )
37 prssi 
 |-  ( ( { K , X } e. E /\ { X , L } e. E ) -> { { K , X } , { X , L } } C_ E )
38 36 37 syl 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> { { K , X } , { X , L } } C_ E )
39 prex 
 |-  { K , y } e. _V
40 prex 
 |-  { y , L } e. _V
41 39 40 prss 
 |-  ( ( { K , y } e. E /\ { y , L } e. E ) <-> { { K , y } , { y , L } } C_ E )
42 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
43 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
44 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
45 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
46 44 45 1 2 gpgvtxel 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( y e. V <-> E. a e. { 0 , 1 } E. b e. ( 0 ..^ 5 ) y = <. a , b >. ) )
47 42 43 46 mp2an 
 |-  ( y e. V <-> E. a e. { 0 , 1 } E. b e. ( 0 ..^ 5 ) y = <. a , b >. )
48 47 biimpi 
 |-  ( y e. V -> E. a e. { 0 , 1 } E. b e. ( 0 ..^ 5 ) y = <. a , b >. )
49 48 adantl 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) -> E. a e. { 0 , 1 } E. b e. ( 0 ..^ 5 ) y = <. a , b >. )
50 opeq1 
 |-  ( a = 0 -> <. a , b >. = <. 0 , b >. )
51 50 eqeq2d 
 |-  ( a = 0 -> ( y = <. a , b >. <-> y = <. 0 , b >. ) )
52 51 adantr 
 |-  ( ( a = 0 /\ ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) ) -> ( y = <. a , b >. <-> y = <. 0 , b >. ) )
53 1 2 3 4 pgnbgreunbgrlem3 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
54 53 adantlr 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) )
55 preq2 
 |-  ( y = <. 0 , b >. -> { K , y } = { K , <. 0 , b >. } )
56 55 eleq1d 
 |-  ( y = <. 0 , b >. -> ( { K , y } e. E <-> { K , <. 0 , b >. } e. E ) )
57 preq1 
 |-  ( y = <. 0 , b >. -> { y , L } = { <. 0 , b >. , L } )
58 57 eleq1d 
 |-  ( y = <. 0 , b >. -> ( { y , L } e. E <-> { <. 0 , b >. , L } e. E ) )
59 56 58 anbi12d 
 |-  ( y = <. 0 , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) <-> ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) ) )
60 eqeq2 
 |-  ( y = <. 0 , b >. -> ( X = y <-> X = <. 0 , b >. ) )
61 59 60 imbi12d 
 |-  ( y = <. 0 , b >. -> ( ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) <-> ( ( { K , <. 0 , b >. } e. E /\ { <. 0 , b >. , L } e. E ) -> X = <. 0 , b >. ) ) )
62 54 61 syl5ibrcom 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) -> ( y = <. 0 , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) )
63 62 adantl 
 |-  ( ( a = 0 /\ ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) ) -> ( y = <. 0 , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) )
64 52 63 sylbid 
 |-  ( ( a = 0 /\ ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) ) -> ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) )
65 64 ex 
 |-  ( a = 0 -> ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) -> ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) ) )
66 1 2 3 4 pgnbgreunbgrlem6 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ b e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
67 66 adantlr 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) -> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) )
68 preq2 
 |-  ( y = <. 1 , b >. -> { K , y } = { K , <. 1 , b >. } )
69 68 eleq1d 
 |-  ( y = <. 1 , b >. -> ( { K , y } e. E <-> { K , <. 1 , b >. } e. E ) )
70 preq1 
 |-  ( y = <. 1 , b >. -> { y , L } = { <. 1 , b >. , L } )
71 70 eleq1d 
 |-  ( y = <. 1 , b >. -> ( { y , L } e. E <-> { <. 1 , b >. , L } e. E ) )
72 69 71 anbi12d 
 |-  ( y = <. 1 , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) <-> ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) ) )
73 eqeq2 
 |-  ( y = <. 1 , b >. -> ( X = y <-> X = <. 1 , b >. ) )
74 72 73 imbi12d 
 |-  ( y = <. 1 , b >. -> ( ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) <-> ( ( { K , <. 1 , b >. } e. E /\ { <. 1 , b >. , L } e. E ) -> X = <. 1 , b >. ) ) )
75 67 74 syl5ibrcom 
 |-  ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) -> ( y = <. 1 , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) )
76 opeq1 
 |-  ( a = 1 -> <. a , b >. = <. 1 , b >. )
77 76 eqeq2d 
 |-  ( a = 1 -> ( y = <. a , b >. <-> y = <. 1 , b >. ) )
78 77 imbi1d 
 |-  ( a = 1 -> ( ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) <-> ( y = <. 1 , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) ) )
79 75 78 imbitrrid 
 |-  ( a = 1 -> ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) -> ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) ) )
80 65 79 jaoi 
 |-  ( ( a = 0 \/ a = 1 ) -> ( ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) /\ b e. ( 0 ..^ 5 ) ) -> ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) ) )
81 80 expd 
 |-  ( ( a = 0 \/ a = 1 ) -> ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) -> ( b e. ( 0 ..^ 5 ) -> ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) ) ) )
82 elpri 
 |-  ( a e. { 0 , 1 } -> ( a = 0 \/ a = 1 ) )
83 81 82 syl11 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) -> ( a e. { 0 , 1 } -> ( b e. ( 0 ..^ 5 ) -> ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) ) ) )
84 83 impd 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) -> ( ( a e. { 0 , 1 } /\ b e. ( 0 ..^ 5 ) ) -> ( y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) ) )
85 84 rexlimdvv 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) -> ( E. a e. { 0 , 1 } E. b e. ( 0 ..^ 5 ) y = <. a , b >. -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) ) )
86 49 85 mpd 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) -> ( ( { K , y } e. E /\ { y , L } e. E ) -> X = y ) )
87 41 86 biimtrrid 
 |-  ( ( ( K e. N /\ L e. N /\ K =/= L ) /\ y e. V ) -> ( { { K , y } , { y , L } } C_ E -> X = y ) )
88 87 ralrimiva 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> A. y e. V ( { { K , y } , { y , L } } C_ E -> X = y ) )
89 38 88 jca 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> ( { { K , X } , { X , L } } C_ E /\ A. y e. V ( { { K , y } , { y , L } } C_ E -> X = y ) ) )
90 12 26 89 rspcedvdw 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> E. x e. V ( { { K , x } , { x , L } } C_ E /\ A. y e. V ( { { K , y } , { y , L } } C_ E -> x = y ) ) )
91 preq2 
 |-  ( x = y -> { K , x } = { K , y } )
92 preq1 
 |-  ( x = y -> { x , L } = { y , L } )
93 91 92 preq12d 
 |-  ( x = y -> { { K , x } , { x , L } } = { { K , y } , { y , L } } )
94 93 sseq1d 
 |-  ( x = y -> ( { { K , x } , { x , L } } C_ E <-> { { K , y } , { y , L } } C_ E ) )
95 94 reu8 
 |-  ( E! x e. V { { K , x } , { x , L } } C_ E <-> E. x e. V ( { { K , x } , { x , L } } C_ E /\ A. y e. V ( { { K , y } , { y , L } } C_ E -> x = y ) ) )
96 90 95 sylibr 
 |-  ( ( K e. N /\ L e. N /\ K =/= L ) -> E! x e. V { { K , x } , { x , L } } C_ E )