Metamath Proof Explorer

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 
|- -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
2 1 pgn4cyclex 
 |-  ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p -> ( # ` f ) =/= 4 )
3 2 imori 
 |-  ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 )
4 3 gen2 
 |-  A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 )
5 2nexaln 
 |-  ( -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) )
6 ianor 
 |-  ( -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ -. ( # ` f ) = 4 ) )
7 df-ne 
 |-  ( ( # ` f ) =/= 4 <-> -. ( # ` f ) = 4 )
8 7 bicomi 
 |-  ( -. ( # ` f ) = 4 <-> ( # ` f ) =/= 4 )
9 8 orbi2i 
 |-  ( ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ -. ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) )
10 6 9 bitri 
 |-  ( -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) )
11 10 2albii 
 |-  ( A. p A. f -. ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) )
12 5 11 bitri 
 |-  ( -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) <-> A. p A. f ( -. f ( Cycles ` ( 5 gPetersenGr 2 ) ) p \/ ( # ` f ) =/= 4 ) )
13 4 12 mpbir 
 |-  -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 )