Metamath Proof Explorer

Theorem gpgvtxel2

Description: The second component of a vertex in a generalized Petersen graph G . (Contributed by AV, 30-Aug-2025)

Ref Expression
Hypotheses gpgvtxel.i 
|- I = ( 0 ..^ N )
gpgvtxel.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgvtxel.g 
|- G = ( N gPetersenGr K )
gpgvtxel.v 
|- V = ( Vtx ` G )
Assertion gpgvtxel2 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( 2nd ` X ) e. I )

Proof

Step Hyp Ref Expression
1 gpgvtxel.i 
 |-  I = ( 0 ..^ N )
2 gpgvtxel.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
3 gpgvtxel.g 
 |-  G = ( N gPetersenGr K )
4 gpgvtxel.v 
 |-  V = ( Vtx ` G )
5 1 2 3 4 gpgvtxel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V <-> E. x e. { 0 , 1 } E. y e. I X = <. x , y >. ) )
6 simpr 
 |-  ( ( x e. { 0 , 1 } /\ y e. I ) -> y e. I )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 op2ndd 
 |-  ( X = <. x , y >. -> ( 2nd ` X ) = y )
10 9 eleq1d 
 |-  ( X = <. x , y >. -> ( ( 2nd ` X ) e. I <-> y e. I ) )
11 6 10 syl5ibrcom 
 |-  ( ( x e. { 0 , 1 } /\ y e. I ) -> ( X = <. x , y >. -> ( 2nd ` X ) e. I ) )
12 11 rexlimivv 
 |-  ( E. x e. { 0 , 1 } E. y e. I X = <. x , y >. -> ( 2nd ` X ) e. I )
13 5 12 biimtrdi 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V -> ( 2nd ` X ) e. I ) )
14 13 imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( 2nd ` X ) e. I )