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 e. UMGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) <-> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) )

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v
 |-  V = ( Vtx ` G )
2 uhgr3cyclex.e
 |-  E = ( Edg ` G )
3 umgrupgr
 |-  ( G e. UMGraph -> G e. UPGraph )
4 3 adantr
 |-  ( ( G e. UMGraph /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) -> G e. UPGraph )
5 simpl
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> f ( Cycles ` G ) p )
6 5 adantl
 |-  ( ( G e. 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 e. UMGraph /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) -> ( # ` f ) = 3 )
9 2 1 upgr3v3e3cycl
 |-  ( ( G e. UPGraph /\ f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) )
10 simpl
 |-  ( ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) -> ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
11 10 reximi
 |-  ( E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) -> E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
12 11 reximi
 |-  ( E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) -> E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
13 12 reximi
 |-  ( E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) -> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
14 9 13 syl
 |-  ( ( G e. UPGraph /\ f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
15 4 6 8 14 syl3anc
 |-  ( ( G e. UMGraph /\ ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) -> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
16 15 ex
 |-  ( G e. UMGraph -> ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) )
17 16 exlimdvv
 |-  ( G e. UMGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) )
18 simplll
 |-  ( ( ( ( G e. UMGraph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) -> G e. UMGraph )
19 df-3an
 |-  ( ( a e. V /\ b e. V /\ c e. V ) <-> ( ( a e. V /\ b e. V ) /\ c e. V ) )
20 19 biimpri
 |-  ( ( ( a e. V /\ b e. V ) /\ c e. V ) -> ( a e. V /\ b e. V /\ c e. V ) )
21 20 ad4ant23
 |-  ( ( ( ( G e. UMGraph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) -> ( a e. V /\ b e. V /\ c e. V ) )
22 simpr
 |-  ( ( ( ( G e. UMGraph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) -> ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) )
23 1 2 umgr3cyclex
 |-  ( ( G e. UMGraph /\ ( a e. V /\ b e. V /\ c e. V ) /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) -> E. f E. 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
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = a ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
26 23 25 syl
 |-  ( ( G e. UMGraph /\ ( a e. V /\ b e. V /\ c e. V ) /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
27 18 21 22 26 syl3anc
 |-  ( ( ( ( G e. UMGraph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) /\ ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
28 27 rexlimdva2
 |-  ( ( G e. UMGraph /\ ( a e. V /\ b e. V ) ) -> ( E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
29 28 rexlimdvva
 |-  ( G e. UMGraph -> ( E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
30 17 29 impbid
 |-  ( G e. UMGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) <-> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) )