Theorem pgjsgr

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

	Ref	Expression
Assertion	pgjsgr	⊢ ( 5 gPetersenGr 2 ) ∈ USGraph

Proof

Step	Hyp	Ref	Expression
1		5eluz3	⊢ 5 ∈ ( ℤ≥ ‘ 3 )
2		pglem	⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
3		gpgusgra	⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 2 ) ∈ USGraph )
4	1 2 3	mp2an	⊢ ( 5 gPetersenGr 2 ) ∈ USGraph