This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )