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 No typesetting found for |- G = ( 5 gPetersenGr 2 ) with typecode |-
Assertion pgn4cyclex ⊢ F Cycles ⁡ G P → F ≠ 4

Proof

Step Hyp Ref Expression
1 pgn4cyclex.g Could not format G = ( 5 gPetersenGr 2 ) : No typesetting found for |- G = ( 5 gPetersenGr 2 ) with typecode |-
2 pgjsgr Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |-
3 1 2 eqeltri ⊢ G ∈ USGraph
4 usgrupgr ⊢ G ∈ USGraph → G ∈ UPGraph
5 3 4 ax-mp ⊢ G ∈ UPGraph
6 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
7 eqid ⊢ Edg ⁡ G = Edg ⁡ G
8 6 7 upgr4cycl4dv4e ⊢ G ∈ UPGraph ∧ F Cycles ⁡ G P ∧ F = 4 → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G ∃ c ∈ Vtx ⁡ G ∃ d ∈ Vtx ⁡ G a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
9 5 8 mp3an1 ⊢ F Cycles ⁡ G P ∧ F = 4 → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G ∃ c ∈ Vtx ⁡ G ∃ d ∈ Vtx ⁡ G a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
10 7 nbusgreledg ⊢ G ∈ USGraph → a ∈ G NeighbVtx b ↔ a b ∈ Edg ⁡ G
11 10 bicomd ⊢ G ∈ USGraph → a b ∈ Edg ⁡ G ↔ a ∈ G NeighbVtx b
12 3 11 ax-mp ⊢ a b ∈ Edg ⁡ G ↔ a ∈ G NeighbVtx b
13 12 biimpi ⊢ a b ∈ Edg ⁡ G → a ∈ G NeighbVtx b
14 13 ad3antrrr ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → a ∈ G NeighbVtx b
15 prcom ⊢ b c = c b
16 15 eleq1i ⊢ b c ∈ Edg ⁡ G ↔ c b ∈ Edg ⁡ G
17 16 biimpi ⊢ b c ∈ Edg ⁡ G → c b ∈ Edg ⁡ G
18 7 nbusgreledg ⊢ G ∈ USGraph → c ∈ G NeighbVtx b ↔ c b ∈ Edg ⁡ G
19 3 18 ax-mp ⊢ c ∈ G NeighbVtx b ↔ c b ∈ Edg ⁡ G
20 17 19 sylibr ⊢ b c ∈ Edg ⁡ G → c ∈ G NeighbVtx b
21 20 ad3antlr ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → c ∈ G NeighbVtx b
22 simprl2 ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → a ≠ c
23 22 adantl ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → a ≠ c
24 eqid ⊢ G NeighbVtx b = G NeighbVtx b
25 1 6 7 24 pgnbgreunbgr ⊢ a ∈ G NeighbVtx b ∧ c ∈ G NeighbVtx b ∧ a ≠ c → ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G
26 14 21 23 25 syl2an23an ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G
27 simpll ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G
28 simplr ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G
29 simpr ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G → b ∈ Vtx ⁡ G
30 simpr ⊢ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G → d ∈ Vtx ⁡ G
31 29 30 anim12i ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G → b ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G
32 simprr2 ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → b ≠ d
33 31 32 anim12i ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → b ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ b ≠ d
34 df-3an ⊢ b ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ b ≠ d ↔ b ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ b ≠ d
35 33 34 sylibr ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → b ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ b ≠ d
36 4cycl2vnunb ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ b ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ b ≠ d → ¬ ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G
37 27 28 35 36 syl2an23an ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → ¬ ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G
38 26 37 pm2.21dd ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → F ≠ 4
39 38 ex ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G → a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → F ≠ 4
40 39 rexlimdvva ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G → ∃ c ∈ Vtx ⁡ G ∃ d ∈ Vtx ⁡ G a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → F ≠ 4
41 40 rexlimivv ⊢ ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G ∃ c ∈ Vtx ⁡ G ∃ d ∈ Vtx ⁡ G a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → F ≠ 4
42 9 41 syl ⊢ F Cycles ⁡ G P ∧ F = 4 → F ≠ 4
43 42 ex ⊢ F Cycles ⁡ G P → F = 4 → F ≠ 4
44 neqne ⊢ ¬ F = 4 → F ≠ 4
45 43 44 pm2.61d1 ⊢ F Cycles ⁡ G P → F ≠ 4