Metamath Proof Explorer

Theorem pglem

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

Ref Expression
Assertion pglem 
|- 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )

Proof

Step Hyp Ref Expression
1 2ex 
 |-  2 e. _V
2 1 prid2 
 |-  2 e. { 1 , 2 }
3 fzo13pr 
 |-  ( 1 ..^ 3 ) = { 1 , 2 }
4 2 3 eleqtrri 
 |-  2 e. ( 1 ..^ 3 )
5 ceil5half3 
 |-  ( |^ ` ( 5 / 2 ) ) = 3
6 5 oveq2i 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ 3 )
7 4 6 eleqtrri 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )