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	⊢ 𝐼 = ( 0 ..^ 𝑁 )
	gpgvtxel.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgvtxel.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	gpgvtxel2	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		gpgvtxel.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		gpgvtxel.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
3		gpgvtxel.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
4		gpgvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
5	1 2 3 4	gpgvtxel	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ 𝐼 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6		simpr	⊢ ( ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	op2ndd	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) = 𝑦 )
10	9	eleq1d	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑋 ) ∈ 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
11	6 10	syl5ibrcom	⊢ ( ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) ∈ 𝐼 ) )
12	11	rexlimivv	⊢ ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ 𝐼 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) ∈ 𝐼 )
13	5 12	biimtrdi	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 → ( 2nd ‘ 𝑋 ) ∈ 𝐼 ) )
14	13	imp	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) ∈ 𝐼 )