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∃pfCycles⁡Gp∧f=3↔∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈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∧fCycles⁡Gp∧f=3→G∈UPGraph
5 simpl ⊢fCycles⁡Gp∧f=3→fCycles⁡Gp
6 5 adantl ⊢G∈UMGraph∧fCycles⁡Gp∧f=3→fCycles⁡Gp
7 simpr ⊢fCycles⁡Gp∧f=3→f=3
8 7 adantl ⊢G∈UMGraph∧fCycles⁡Gp∧f=3→f=3
9 2 1 upgr3v3e3cycl ⊢G∈UPGraph∧fCycles⁡Gp∧f=3→∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E∧a≠b∧b≠c∧c≠a
10 simpl ⊢ab∈E∧bc∈E∧ca∈E∧a≠b∧b≠c∧c≠a→ab∈E∧bc∈E∧ca∈E
11 10 reximi ⊢∃c∈Vab∈E∧bc∈E∧ca∈E∧a≠b∧b≠c∧c≠a→∃c∈Vab∈E∧bc∈E∧ca∈E
12 11 reximi ⊢∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E∧a≠b∧b≠c∧c≠a→∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
13 12 reximi ⊢∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E∧a≠b∧b≠c∧c≠a→∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
14 9 13 syl ⊢G∈UPGraph∧fCycles⁡Gp∧f=3→∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
15 4 6 8 14 syl3anc ⊢G∈UMGraph∧fCycles⁡Gp∧f=3→∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
16 15 ex ⊢G∈UMGraph→fCycles⁡Gp∧f=3→∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
17 16 exlimdvv ⊢G∈UMGraph→∃f∃pfCycles⁡Gp∧f=3→∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E
18 simplll ⊢G∈UMGraph∧a∈V∧b∈V∧c∈V∧ab∈E∧bc∈E∧ca∈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∧ab∈E∧bc∈E∧ca∈E→a∈V∧b∈V∧c∈V
22 simpr ⊢G∈UMGraph∧a∈V∧b∈V∧c∈V∧ab∈E∧bc∈E∧ca∈E→ab∈E∧bc∈E∧ca∈E
23 1 2 umgr3cyclex ⊢G∈UMGraph∧a∈V∧b∈V∧c∈V∧ab∈E∧bc∈E∧ca∈E→∃f∃pfCycles⁡Gp∧f=3∧p⁡0=a
24 3simpa ⊢fCycles⁡Gp∧f=3∧p⁡0=a→fCycles⁡Gp∧f=3
25 24 2eximi ⊢∃f∃pfCycles⁡Gp∧f=3∧p⁡0=a→∃f∃pfCycles⁡Gp∧f=3
26 23 25 syl ⊢G∈UMGraph∧a∈V∧b∈V∧c∈V∧ab∈E∧bc∈E∧ca∈E→∃f∃pfCycles⁡Gp∧f=3
27 18 21 22 26 syl3anc ⊢G∈UMGraph∧a∈V∧b∈V∧c∈V∧ab∈E∧bc∈E∧ca∈E→∃f∃pfCycles⁡Gp∧f=3
28 27 rexlimdva2 ⊢G∈UMGraph∧a∈V∧b∈V→∃c∈Vab∈E∧bc∈E∧ca∈E→∃f∃pfCycles⁡Gp∧f=3
29 28 rexlimdvva ⊢G∈UMGraph→∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E→∃f∃pfCycles⁡Gp∧f=3
30 17 29 impbid ⊢G∈UMGraph→∃f∃pfCycles⁡Gp∧f=3↔∃a∈V∃b∈V∃c∈Vab∈E∧bc∈E∧ca∈E