Metamath Proof Explorer

Theorem umgr2cycllem

Description: Lemma for umgr2cycl . (Contributed by BTernaryTau, 17-Oct-2023)

Ref Expression
Hypotheses umgr2cycllem.1 
|- F = <" J K ">
umgr2cycllem.2 
|- I = ( iEdg ` G )
umgr2cycllem.3 
|- ( ph -> G e. UMGraph )
umgr2cycllem.4 
|- ( ph -> J e. dom I )
umgr2cycllem.5 
|- ( ph -> J =/= K )
umgr2cycllem.6 
|- ( ph -> ( I ` J ) = ( I ` K ) )
Assertion umgr2cycllem 
|- ( ph -> E. p F ( Cycles ` G ) p )

Proof

Step Hyp Ref Expression
1 umgr2cycllem.1 
 |-  F = <" J K ">
2 umgr2cycllem.2 
 |-  I = ( iEdg ` G )
3 umgr2cycllem.3 
 |-  ( ph -> G e. UMGraph )
4 umgr2cycllem.4 
 |-  ( ph -> J e. dom I )
5 umgr2cycllem.5 
 |-  ( ph -> J =/= K )
6 umgr2cycllem.6 
 |-  ( ph -> ( I ` J ) = ( I ` K ) )
7 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
8 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
9 3 7 8 3syl 
 |-  ( ph -> Fun I )
10 2 iedgedg 
 |-  ( ( Fun I /\ J e. dom I ) -> ( I ` J ) e. ( Edg ` G ) )
11 9 4 10 syl2anc 
 |-  ( ph -> ( I ` J ) e. ( Edg ` G ) )
12 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
13 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
14 12 13 umgredg 
 |-  ( ( G e. UMGraph /\ ( I ` J ) e. ( Edg ` G ) ) -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) )
15 3 11 14 syl2anc 
 |-  ( ph -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) )
16 ax-5 
 |-  ( a e. ( Vtx ` G ) -> A. b a e. ( Vtx ` G ) )
17 alral 
 |-  ( A. b a e. ( Vtx ` G ) -> A. b e. ( Vtx ` G ) a e. ( Vtx ` G ) )
18 16 17 syl 
 |-  ( a e. ( Vtx ` G ) -> A. b e. ( Vtx ` G ) a e. ( Vtx ` G ) )
19 r19.29 
 |-  ( ( A. b e. ( Vtx ` G ) a e. ( Vtx ` G ) /\ E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. b e. ( Vtx ` G ) ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) )
20 18 19 sylan 
 |-  ( ( a e. ( Vtx ` G ) /\ E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. b e. ( Vtx ` G ) ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) )
21 eqid 
 |-  <" a b a "> = <" a b a ">
22 simp2 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) )
23 simp3l 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> a =/= b )
24 eqimss2 
 |-  ( ( I ` J ) = { a , b } -> { a , b } C_ ( I ` J ) )
25 24 adantl 
 |-  ( ( a =/= b /\ ( I ` J ) = { a , b } ) -> { a , b } C_ ( I ` J ) )
26 25 3ad2ant3 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> { a , b } C_ ( I ` J ) )
27 6 sseq2d 
 |-  ( ph -> ( { a , b } C_ ( I ` J ) <-> { a , b } C_ ( I ` K ) ) )
28 24 27 syl5ib 
 |-  ( ph -> ( ( I ` J ) = { a , b } -> { a , b } C_ ( I ` K ) ) )
29 28 adantld 
 |-  ( ph -> ( ( a =/= b /\ ( I ` J ) = { a , b } ) -> { a , b } C_ ( I ` K ) ) )
30 29 adantld 
 |-  ( ph -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> { a , b } C_ ( I ` K ) ) )
31 30 3impib 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> { a , b } C_ ( I ` K ) )
32 26 31 jca 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( { a , b } C_ ( I ` J ) /\ { a , b } C_ ( I ` K ) ) )
33 5 3ad2ant1 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> J =/= K )
34 21 1 22 23 32 12 2 33 2cycl2d 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> F ( Cycles ` G ) <" a b a "> )
35 34 3expib 
 |-  ( ph -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> F ( Cycles ` G ) <" a b a "> ) )
36 35 exp4c 
 |-  ( ph -> ( a e. ( Vtx ` G ) -> ( b e. ( Vtx ` G ) -> ( ( a =/= b /\ ( I ` J ) = { a , b } ) -> F ( Cycles ` G ) <" a b a "> ) ) ) )
37 36 com23 
 |-  ( ph -> ( b e. ( Vtx ` G ) -> ( a e. ( Vtx ` G ) -> ( ( a =/= b /\ ( I ` J ) = { a , b } ) -> F ( Cycles ` G ) <" a b a "> ) ) ) )
38 37 imp4a 
 |-  ( ph -> ( b e. ( Vtx ` G ) -> ( ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> F ( Cycles ` G ) <" a b a "> ) ) )
39 s3cli 
 |-  <" a b a "> e. Word _V
40 breq2 
 |-  ( p = <" a b a "> -> ( F ( Cycles ` G ) p <-> F ( Cycles ` G ) <" a b a "> ) )
41 40 rspcev 
 |-  ( ( <" a b a "> e. Word _V /\ F ( Cycles ` G ) <" a b a "> ) -> E. p e. Word _V F ( Cycles ` G ) p )
42 39 41 mpan 
 |-  ( F ( Cycles ` G ) <" a b a "> -> E. p e. Word _V F ( Cycles ` G ) p )
43 rexex 
 |-  ( E. p e. Word _V F ( Cycles ` G ) p -> E. p F ( Cycles ` G ) p )
44 42 43 syl 
 |-  ( F ( Cycles ` G ) <" a b a "> -> E. p F ( Cycles ` G ) p )
45 38 44 syl8 
 |-  ( ph -> ( b e. ( Vtx ` G ) -> ( ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. p F ( Cycles ` G ) p ) ) )
46 45 rexlimdv 
 |-  ( ph -> ( E. b e. ( Vtx ` G ) ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. p F ( Cycles ` G ) p ) )
47 20 46 syl5 
 |-  ( ph -> ( ( a e. ( Vtx ` G ) /\ E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. p F ( Cycles ` G ) p ) )
48 47 expd 
 |-  ( ph -> ( a e. ( Vtx ` G ) -> ( E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) -> E. p F ( Cycles ` G ) p ) ) )
49 48 rexlimdv 
 |-  ( ph -> ( E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) -> E. p F ( Cycles ` G ) p ) )
50 15 49 mpd 
 |-  ( ph -> E. p F ( Cycles ` G ) p )