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	Could not format assertion : No typesetting found for |- -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	Could not format ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) with typecode |-
2	1	pgn4cyclex	Could not format ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p -> ( # ` f ) =/= 4 ) : No typesetting found for |- ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p -> ( # ` f ) =/= 4 ) with typecode |-
3	2	imori	Could not format ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) : No typesetting found for |- ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) with typecode |-
4	3	gen2	Could not format A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) : No typesetting found for |- A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) with typecode |-
5		2nexaln	Could not format ( -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) ) : No typesetting found for |- ( -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) ) with typecode |-
6		ianor	Could not format ( -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ -. ( # ` f ) = 4 ) ) : No typesetting found for |- ( -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ -. ( # ` f ) = 4 ) ) with typecode |-
7		df-ne	$$⊢\left|f\right|\ne 4\leftrightarrow \neg \left|f\right|=4$$
8	7	bicomi	$$⊢\neg \left|f\right|=4\leftrightarrow \left|f\right|\ne 4$$
9	8	orbi2i	Could not format ( ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ -. ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) : No typesetting found for |- ( ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ -. ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) with typecode |-
10	6 9	bitri	Could not format ( -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) : No typesetting found for |- ( -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) with typecode |-
11	10	2albii	Could not format ( A. p A. f -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) : No typesetting found for |- ( A. p A. f -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) with typecode |-
12	5 11	bitri	Could not format ( -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) : No typesetting found for |- ( -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) ) with typecode |-
13	4 12	mpbir	Could not format -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) : No typesetting found for |- -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) with typecode |-