Metamath Proof Explorer

Theorem pgjsgr

Description: A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025)

Ref Expression
Assertion pgjsgr 
|- ( 5 gPetersenGr 2 ) e. USGraph

Proof

Step Hyp Ref Expression
1 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
2 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
3 gpgusgra 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph )
4 1 2 3 mp2an 
 |-  ( 5 gPetersenGr 2 ) e. USGraph