Metamath Proof Explorer

Theorem opgpgvtx

Description: A vertex in a generalized Petersen graph G as ordered pair. (Contributed by AV, 1-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 opgpgvtx.i 
 |-  I = ( 0 ..^ N )
2 opgpgvtx.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
3 opgpgvtx.g 
 |-  G = ( N gPetersenGr K )
4 opgpgvtx.v 
 |-  V = ( Vtx ` G )
5 3 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) )
6 4 5 eqtri 
 |-  V = ( Vtx ` ( N gPetersenGr K ) )
7 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
8 2 1 gpgvtx 
 |-  ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) )
9 7 8 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) )
10 6 9 eqtrid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> V = ( { 0 , 1 } X. I ) )
11 10 eleq2d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( <. X , Y >. e. V <-> <. X , Y >. e. ( { 0 , 1 } X. I ) ) )
12 opelxp 
 |-  ( <. X , Y >. e. ( { 0 , 1 } X. I ) <-> ( X e. { 0 , 1 } /\ Y e. I ) )
13 12 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( <. X , Y >. e. ( { 0 , 1 } X. I ) <-> ( X e. { 0 , 1 } /\ Y e. I ) ) )
14 c0ex 
 |-  0 e. _V
15 1ex 
 |-  1 e. _V
16 14 15 elpr2 
 |-  ( X e. { 0 , 1 } <-> ( X = 0 \/ X = 1 ) )
17 16 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. { 0 , 1 } <-> ( X = 0 \/ X = 1 ) ) )
18 17 anbi1d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( X e. { 0 , 1 } /\ Y e. I ) <-> ( ( X = 0 \/ X = 1 ) /\ Y e. I ) ) )
19 11 13 18 3bitrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( <. X , Y >. e. V <-> ( ( X = 0 \/ X = 1 ) /\ Y e. I ) ) )