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 simp2l 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> a e. ( Vtx ` G ) )
23 simp2r 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> b e. ( Vtx ` G ) )
24 22 23 22 3jca 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ a e. ( Vtx ` G ) ) )
25 simp3l 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> a =/= b )
26 25 necomd 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> b =/= a )
27 25 26 jca 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( a =/= b /\ b =/= a ) )
28 simp3r 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( I ` J ) = { a , b } )
29 28 eqimsscd 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> { a , b } C_ ( I ` J ) )
30 6 3ad2ant1 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( I ` J ) = ( I ` K ) )
31 30 28 eqtr3d 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( I ` K ) = { a , b } )
32 prcom 
 |-  { a , b } = { b , a }
33 32 a1i 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> { a , b } = { b , a } )
34 31 33 eqtrd 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( I ` K ) = { b , a } )
35 eqimss2 
 |-  ( ( I ` K ) = { b , a } -> { b , a } C_ ( I ` K ) )
36 34 35 syl 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> { b , a } C_ ( I ` K ) )
37 29 36 jca 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> ( { a , b } C_ ( I ` J ) /\ { b , a } C_ ( I ` K ) ) )
38 5 3ad2ant1 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> J =/= K )
39 eqidd 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> a = a )
40 21 1 24 27 37 12 2 38 39 2cycld 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> F ( Cycles ` G ) <" a b a "> )
41 40 3expib 
 |-  ( ph -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> F ( Cycles ` G ) <" a b a "> ) )
42 41 exp4c 
 |-  ( ph -> ( a e. ( Vtx ` G ) -> ( b e. ( Vtx ` G ) -> ( ( a =/= b /\ ( I ` J ) = { a , b } ) -> F ( Cycles ` G ) <" a b a "> ) ) ) )
43 42 com23 
 |-  ( ph -> ( b e. ( Vtx ` G ) -> ( a e. ( Vtx ` G ) -> ( ( a =/= b /\ ( I ` J ) = { a , b } ) -> F ( Cycles ` G ) <" a b a "> ) ) ) )
44 43 imp4a 
 |-  ( ph -> ( b e. ( Vtx ` G ) -> ( ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> F ( Cycles ` G ) <" a b a "> ) ) )
45 s3cli 
 |-  <" a b a "> e. Word _V
46 breq2 
 |-  ( p = <" a b a "> -> ( F ( Cycles ` G ) p <-> F ( Cycles ` G ) <" a b a "> ) )
47 46 rspcev 
 |-  ( ( <" a b a "> e. Word _V /\ F ( Cycles ` G ) <" a b a "> ) -> E. p e. Word _V F ( Cycles ` G ) p )
48 45 47 mpan 
 |-  ( F ( Cycles ` G ) <" a b a "> -> E. p e. Word _V F ( Cycles ` G ) p )
49 rexex 
 |-  ( E. p e. Word _V F ( Cycles ` G ) p -> E. p F ( Cycles ` G ) p )
50 48 49 syl 
 |-  ( F ( Cycles ` G ) <" a b a "> -> E. p F ( Cycles ` G ) p )
51 44 50 syl8 
 |-  ( ph -> ( b e. ( Vtx ` G ) -> ( ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. p F ( Cycles ` G ) p ) ) )
52 51 rexlimdv 
 |-  ( ph -> ( E. b e. ( Vtx ` G ) ( a e. ( Vtx ` G ) /\ ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. p F ( Cycles ` G ) p ) )
53 20 52 syl5 
 |-  ( ph -> ( ( a e. ( Vtx ` G ) /\ E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) ) -> E. p F ( Cycles ` G ) p ) )
54 53 expd 
 |-  ( ph -> ( a e. ( Vtx ` G ) -> ( E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) -> E. p F ( Cycles ` G ) p ) ) )
55 54 rexlimdv 
 |-  ( ph -> ( E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) ( a =/= b /\ ( I ` J ) = { a , b } ) -> E. p F ( Cycles ` G ) p ) )
56 15 55 mpd 
 |-  ( ph -> E. p F ( Cycles ` G ) p )