Theorem pglem

Description: Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025)

	Ref	Expression
Assertion	pglem	⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2ex	⊢ 2 ∈ V
2	1	prid2	⊢ 2 ∈ { 1 , 2 }
3		fzo13pr	⊢ ( 1 ..^ 3 ) = { 1 , 2 }
4	2 3	eleqtrri	⊢ 2 ∈ ( 1 ..^ 3 )
5		ceil5half3	⊢ ( ⌈ ‘ ( 5 / 2 ) ) = 3
6	5	oveq2i	⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ 3 )
7	4 6	eleqtrri	⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )