Metamath Proof Explorer

Theorem pgn4cyclex

Description: A cycle in a Petersen graph does not have length 4. (Contributed by AV, 9-Nov-2025)

Ref Expression
Hypothesis pgn4cyclex.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
Assertion pgn4cyclex ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≠ 4 )

Proof

Step Hyp Ref Expression
1 pgn4cyclex.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
2 pgjsgr ⊢ ( 5 gPetersenGr 2 ) ∈ USGraph
3 1 2 eqeltri ⊢ 𝐺 ∈ USGraph
4 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
5 3 4 ax-mp ⊢ 𝐺 ∈ UPGraph
6 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
8 6 7 upgr4cycl4dv4e ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) )
9 5 8 mp3an1 ⊢ ( ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) )
10 7 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) )
11 10 bicomd ⊢ ( 𝐺 ∈ USGraph → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
12 3 11 ax-mp ⊢ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
13 12 biimpi ⊢ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) → 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
14 13 ad3antrrr ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
15 prcom ⊢ { 𝑏 , 𝑐 } = { 𝑐 , 𝑏 }
16 15 eleq1i ⊢ ( { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑐 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) )
17 16 biimpi ⊢ ( { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) → { 𝑐 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) )
18 7 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑐 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ { 𝑐 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) )
19 3 18 ax-mp ⊢ ( 𝑐 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ { 𝑐 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) )
20 17 19 sylibr ⊢ ( { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) → 𝑐 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
21 20 ad3antlr ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑐 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
22 simprl2 ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑎 ≠ 𝑐 )
23 22 adantl ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → 𝑎 ≠ 𝑐 )
24 eqid ⊢ ( 𝐺 NeighbVtx 𝑏 ) = ( 𝐺 NeighbVtx 𝑏 )
25 1 6 7 24 pgnbgreunbgr ⊢ ( ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ∧ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑏 ) ∧ 𝑎 ≠ 𝑐 ) → ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
26 14 21 23 25 syl2an23an ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
27 simpll ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
28 simplr ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
29 simpr ⊢ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
30 simpr ⊢ ( ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑑 ∈ ( Vtx ‘ 𝐺 ) )
31 29 30 anim12i ⊢ ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) )
32 simprr2 ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑏 ≠ 𝑑 )
33 31 32 anim12i ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑏 ≠ 𝑑 ) )
34 df-3an ⊢ ( ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ≠ 𝑑 ) ↔ ( ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑏 ≠ 𝑑 ) )
35 33 34 sylibr ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ≠ 𝑑 ) )
36 4cycl2vnunb ⊢ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ≠ 𝑑 ) ) → ¬ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
37 27 28 35 36 syl2an23an ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ¬ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
38 26 37 pm2.21dd ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 )
39 38 ex ⊢ ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
40 39 rexlimdvva ⊢ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) → ( ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
41 40 rexlimivv ⊢ ( ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 )
42 9 41 syl ⊢ ( ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) → ( ♯ ‘ 𝐹 ) ≠ 4 )
43 42 ex ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 4 → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
44 neqne ⊢ ( ¬ ( ♯ ‘ 𝐹 ) = 4 → ( ♯ ‘ 𝐹 ) ≠ 4 )
45 43 44 pm2.61d1 ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≠ 4 )