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	⊢ 𝐼 = ( 0 ..^ 𝑁 )
	opgpgvtx.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	opgpgvtx.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	opgpgvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	opgpgvtx	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑉 ↔ ( ( 𝑋 = 0 ∨ 𝑋 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opgpgvtx.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		opgpgvtx.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
3		opgpgvtx.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
4		opgpgvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
5	3	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
6	4 5	eqtri	⊢ 𝑉 = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
7		eluzge3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
8	2 1	gpgvtx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × 𝐼 ) )
9	7 8	sylan	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × 𝐼 ) )
10	6 9	eqtrid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑉 = ( { 0 , 1 } × 𝐼 ) )
11	10	eleq2d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑉 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 0 , 1 } × 𝐼 ) ) )
12		opelxp	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 0 , 1 } × 𝐼 ) ↔ ( 𝑋 ∈ { 0 , 1 } ∧ 𝑌 ∈ 𝐼 ) )
13	12	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 0 , 1 } × 𝐼 ) ↔ ( 𝑋 ∈ { 0 , 1 } ∧ 𝑌 ∈ 𝐼 ) ) )
14		c0ex	⊢ 0 ∈ V
15		1ex	⊢ 1 ∈ V
16	14 15	elpr2	⊢ ( 𝑋 ∈ { 0 , 1 } ↔ ( 𝑋 = 0 ∨ 𝑋 = 1 ) )
17	16	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ { 0 , 1 } ↔ ( 𝑋 = 0 ∨ 𝑋 = 1 ) ) )
18	17	anbi1d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( 𝑋 ∈ { 0 , 1 } ∧ 𝑌 ∈ 𝐼 ) ↔ ( ( 𝑋 = 0 ∨ 𝑋 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )
19	11 13 18	3bitrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑉 ↔ ( ( 𝑋 = 0 ∨ 𝑋 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )