Metamath Proof Explorer

Theorem umgr3v3e3cycl

Description: If and only if there is a 3-cycle in a multigraph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017) (Revised by AV, 12-Feb-2021)

Ref Expression
Hypotheses uhgr3cyclex.v ⊢ V = Vtx ⁡ G
uhgr3cyclex.e ⊢ E = Edg ⁡ G
Assertion umgr3v3e3cycl ⊢ G ∈ UMGraph → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v ⊢ V = Vtx ⁡ G
2 uhgr3cyclex.e ⊢ E = Edg ⁡ G
3 umgrupgr ⊢ G ∈ UMGraph → G ∈ UPGraph
4 3 adantr ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ f = 3 → G ∈ UPGraph
5 simpl ⊢ f Cycles ⁡ G p ∧ f = 3 → f Cycles ⁡ G p
6 5 adantl ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ f = 3 → f Cycles ⁡ G p
7 simpr ⊢ f Cycles ⁡ G p ∧ f = 3 → f = 3
8 7 adantl ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ f = 3 → f = 3
9 2 1 upgr3v3e3cycl ⊢ G ∈ UPGraph ∧ f Cycles ⁡ G p ∧ f = 3 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a
10 simpl ⊢ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a → a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
11 10 reximi ⊢ ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a → ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
12 11 reximi ⊢ ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a → ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
13 12 reximi ⊢ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
14 9 13 syl ⊢ G ∈ UPGraph ∧ f Cycles ⁡ G p ∧ f = 3 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
15 4 6 8 14 syl3anc ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ f = 3 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
16 15 ex ⊢ G ∈ UMGraph → f Cycles ⁡ G p ∧ f = 3 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
17 16 exlimdvv ⊢ G ∈ UMGraph → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
18 simplll ⊢ G ∈ UMGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → G ∈ UMGraph
19 df-3an ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V ↔ a ∈ V ∧ b ∈ V ∧ c ∈ V
20 19 biimpri ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V → a ∈ V ∧ b ∈ V ∧ c ∈ V
21 20 ad4ant23 ⊢ G ∈ UMGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → a ∈ V ∧ b ∈ V ∧ c ∈ V
22 simpr ⊢ G ∈ UMGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → a b ∈ E ∧ b c ∈ E ∧ c a ∈ E
23 1 2 umgr3cyclex ⊢ G ∈ UMGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = a
24 3simpa ⊢ f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = a → f Cycles ⁡ G p ∧ f = 3
25 24 2eximi ⊢ ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = a → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3
26 23 25 syl ⊢ G ∈ UMGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3
27 18 21 22 26 syl3anc ⊢ G ∈ UMGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3
28 27 rexlimdva2 ⊢ G ∈ UMGraph ∧ a ∈ V ∧ b ∈ V → ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3
29 28 rexlimdvva ⊢ G ∈ UMGraph → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3
30 17 29 impbid ⊢ G ∈ UMGraph → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a b ∈ E ∧ b c ∈ E ∧ c a ∈ E