Theorem pg4cyclnex

Description: In the Petersen graph G(5,2), there is no cycle of length 4. (Contributed by AV, 22-Nov-2025)

	Ref	Expression
Assertion	pg4cyclnex	⊢ ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
2	1	pgn4cyclex	⊢ ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 → ( ♯ ‘ 𝑓 ) ≠ 4 )
3	2	imori	⊢ ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ( ♯ ‘ 𝑓 ) ≠ 4 )
4	3	gen2	⊢ ∀ 𝑝 ∀ 𝑓 ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ( ♯ ‘ 𝑓 ) ≠ 4 )
5		2nexaln	⊢ ( ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ↔ ∀ 𝑝 ∀ 𝑓 ¬ ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) )
6		ianor	⊢ ( ¬ ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ↔ ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ¬ ( ♯ ‘ 𝑓 ) = 4 ) )
7		df-ne	⊢ ( ( ♯ ‘ 𝑓 ) ≠ 4 ↔ ¬ ( ♯ ‘ 𝑓 ) = 4 )
8	7	bicomi	⊢ ( ¬ ( ♯ ‘ 𝑓 ) = 4 ↔ ( ♯ ‘ 𝑓 ) ≠ 4 )
9	8	orbi2i	⊢ ( ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ¬ ( ♯ ‘ 𝑓 ) = 4 ) ↔ ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ( ♯ ‘ 𝑓 ) ≠ 4 ) )
10	6 9	bitri	⊢ ( ¬ ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ↔ ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ( ♯ ‘ 𝑓 ) ≠ 4 ) )
11	10	2albii	⊢ ( ∀ 𝑝 ∀ 𝑓 ¬ ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ↔ ∀ 𝑝 ∀ 𝑓 ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ( ♯ ‘ 𝑓 ) ≠ 4 ) )
12	5 11	bitri	⊢ ( ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ↔ ∀ 𝑝 ∀ 𝑓 ( ¬ 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∨ ( ♯ ‘ 𝑓 ) ≠ 4 ) )
13	4 12	mpbir	⊢ ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 )