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 No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
opgpgvtx.v V = Vtx G
Assertion opgpgvtx N 3 K J X Y V X = 0 X = 1 Y I

Proof

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