Theorem gpgvtxel

Description: A vertex in a generalized Petersen graph G . (Contributed by AV, 29-Aug-2025)

	Ref	Expression
Hypotheses	gpgvtxel.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
	gpgvtxel.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgvtxel.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	gpgvtxel	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ 𝐼 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		gpgvtxel.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		gpgvtxel.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
3		gpgvtxel.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
4		gpgvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
5	3	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
6	4 5	eqtri	⊢ 𝑉 = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
7	6	eleq2i	⊢ ( 𝑋 ∈ 𝑉 ↔ 𝑋 ∈ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) )
8		eluz3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
9	2 1	gpgvtx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × 𝐼 ) )
10	9	eleq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ↔ 𝑋 ∈ ( { 0 , 1 } × 𝐼 ) ) )
11	8 10	sylan	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ↔ 𝑋 ∈ ( { 0 , 1 } × 𝐼 ) ) )
12	7 11	bitrid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ 𝑋 ∈ ( { 0 , 1 } × 𝐼 ) ) )
13		elxp2	⊢ ( 𝑋 ∈ ( { 0 , 1 } × 𝐼 ) ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ 𝐼 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ )
14	12 13	bitrdi	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ 𝐼 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )