Metamath Proof Explorer

Theorem loop1cycl

Description: A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023)

Ref Expression
Assertion loop1cycl 
|- ( G e. UHGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) <-> { A } e. ( Edg ` G ) ) )

Proof

Step Hyp Ref Expression
1 cyclprop 
 |-  ( f ( Cycles ` G ) p -> ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) )
2 fveq2 
 |-  ( ( # ` f ) = 1 -> ( p ` ( # ` f ) ) = ( p ` 1 ) )
3 2 eqeq2d 
 |-  ( ( # ` f ) = 1 -> ( ( p ` 0 ) = ( p ` ( # ` f ) ) <-> ( p ` 0 ) = ( p ` 1 ) ) )
4 3 anbi2d 
 |-  ( ( # ` f ) = 1 -> ( ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) <-> ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) ) )
5 4 biimpd 
 |-  ( ( # ` f ) = 1 -> ( ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) -> ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) ) )
6 1 5 mpan9 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) -> ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) )
7 pthiswlk 
 |-  ( f ( Paths ` G ) p -> f ( Walks ` G ) p )
8 7 anim1i 
 |-  ( ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) -> ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) )
9 6 8 syl 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) -> ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) )
10 9 anim1i 
 |-  ( ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) /\ ( # ` f ) = 1 ) -> ( ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) /\ ( # ` f ) = 1 ) )
11 10 anabss3 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) -> ( ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) /\ ( # ` f ) = 1 ) )
12 df-3an 
 |-  ( ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) /\ ( # ` f ) = 1 ) <-> ( ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) ) /\ ( # ` f ) = 1 ) )
13 11 12 sylibr 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) -> ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) /\ ( # ` f ) = 1 ) )
14 3ancomb 
 |-  ( ( f ( Walks ` G ) p /\ ( p ` 0 ) = ( p ` 1 ) /\ ( # ` f ) = 1 ) <-> ( f ( Walks ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = ( p ` 1 ) ) )
15 13 14 sylib 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) -> ( f ( Walks ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = ( p ` 1 ) ) )
16 wlkl1loop 
 |-  ( ( ( Fun ( iEdg ` G ) /\ f ( Walks ` G ) p ) /\ ( ( # ` f ) = 1 /\ ( p ` 0 ) = ( p ` 1 ) ) ) -> { ( p ` 0 ) } e. ( Edg ` G ) )
17 16 expl 
 |-  ( Fun ( iEdg ` G ) -> ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 1 /\ ( p ` 0 ) = ( p ` 1 ) ) ) -> { ( p ` 0 ) } e. ( Edg ` G ) ) )
18 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
19 18 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
20 17 19 syl11 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 1 /\ ( p ` 0 ) = ( p ` 1 ) ) ) -> ( G e. UHGraph -> { ( p ` 0 ) } e. ( Edg ` G ) ) )
21 20 3impb 
 |-  ( ( f ( Walks ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = ( p ` 1 ) ) -> ( G e. UHGraph -> { ( p ` 0 ) } e. ( Edg ` G ) ) )
22 15 21 syl 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) -> ( G e. UHGraph -> { ( p ` 0 ) } e. ( Edg ` G ) ) )
23 22 3adant3 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) -> ( G e. UHGraph -> { ( p ` 0 ) } e. ( Edg ` G ) ) )
24 sneq 
 |-  ( ( p ` 0 ) = A -> { ( p ` 0 ) } = { A } )
25 24 eleq1d 
 |-  ( ( p ` 0 ) = A -> ( { ( p ` 0 ) } e. ( Edg ` G ) <-> { A } e. ( Edg ` G ) ) )
26 25 3ad2ant3 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) -> ( { ( p ` 0 ) } e. ( Edg ` G ) <-> { A } e. ( Edg ` G ) ) )
27 23 26 sylibd 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) -> ( G e. UHGraph -> { A } e. ( Edg ` G ) ) )
28 27 exlimivv 
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) -> ( G e. UHGraph -> { A } e. ( Edg ` G ) ) )
29 28 com12 
 |-  ( G e. UHGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) -> { A } e. ( Edg ` G ) ) )
30 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
31 30 eleq2i 
 |-  ( { A } e. ( Edg ` G ) <-> { A } e. ran ( iEdg ` G ) )
32 elrnrexdm 
 |-  ( Fun ( iEdg ` G ) -> ( { A } e. ran ( iEdg ` G ) -> E. j e. dom ( iEdg ` G ) { A } = ( ( iEdg ` G ) ` j ) ) )
33 eqcom 
 |-  ( { A } = ( ( iEdg ` G ) ` j ) <-> ( ( iEdg ` G ) ` j ) = { A } )
34 33 rexbii 
 |-  ( E. j e. dom ( iEdg ` G ) { A } = ( ( iEdg ` G ) ` j ) <-> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { A } )
35 32 34 syl6ib 
 |-  ( Fun ( iEdg ` G ) -> ( { A } e. ran ( iEdg ` G ) -> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { A } ) )
36 31 35 syl5bi 
 |-  ( Fun ( iEdg ` G ) -> ( { A } e. ( Edg ` G ) -> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { A } ) )
37 19 36 syl 
 |-  ( G e. UHGraph -> ( { A } e. ( Edg ` G ) -> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { A } ) )
38 df-rex 
 |-  ( E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { A } <-> E. j ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = { A } ) )
39 37 38 syl6ib 
 |-  ( G e. UHGraph -> ( { A } e. ( Edg ` G ) -> E. j ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = { A } ) ) )
40 18 lp1cycl 
 |-  ( ( G e. UHGraph /\ j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = { A } ) -> <" j "> ( Cycles ` G ) <" A A "> )
41 40 3expib 
 |-  ( G e. UHGraph -> ( ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = { A } ) -> <" j "> ( Cycles ` G ) <" A A "> ) )
42 41 eximdv 
 |-  ( G e. UHGraph -> ( E. j ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = { A } ) -> E. j <" j "> ( Cycles ` G ) <" A A "> ) )
43 39 42 syld 
 |-  ( G e. UHGraph -> ( { A } e. ( Edg ` G ) -> E. j <" j "> ( Cycles ` G ) <" A A "> ) )
44 s1len 
 |-  ( # ` <" j "> ) = 1
45 44 ax-gen 
 |-  A. j ( # ` <" j "> ) = 1
46 19.29r 
 |-  ( ( E. j <" j "> ( Cycles ` G ) <" A A "> /\ A. j ( # ` <" j "> ) = 1 ) -> E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) )
47 45 46 mpan2 
 |-  ( E. j <" j "> ( Cycles ` G ) <" A A "> -> E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) )
48 43 47 syl6 
 |-  ( G e. UHGraph -> ( { A } e. ( Edg ` G ) -> E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) ) )
49 48 imp 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) )
50 uhgredgn0 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> { A } e. ( ~P ( Vtx ` G ) \ { (/) } ) )
51 eldifsni 
 |-  ( { A } e. ( ~P ( Vtx ` G ) \ { (/) } ) -> { A } =/= (/) )
52 50 51 syl 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> { A } =/= (/) )
53 snnzb 
 |-  ( A e. _V <-> { A } =/= (/) )
54 52 53 sylibr 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> A e. _V )
55 s2fv0 
 |-  ( A e. _V -> ( <" A A "> ` 0 ) = A )
56 54 55 syl 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> ( <" A A "> ` 0 ) = A )
57 56 alrimiv 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> A. j ( <" A A "> ` 0 ) = A )
58 19.29r 
 |-  ( ( E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) /\ A. j ( <" A A "> ` 0 ) = A ) -> E. j ( ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) /\ ( <" A A "> ` 0 ) = A ) )
59 49 57 58 syl2anc 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> E. j ( ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) /\ ( <" A A "> ` 0 ) = A ) )
60 df-3an 
 |-  ( ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) <-> ( ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) /\ ( <" A A "> ` 0 ) = A ) )
61 60 exbii 
 |-  ( E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) <-> E. j ( ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 ) /\ ( <" A A "> ` 0 ) = A ) )
62 59 61 sylibr 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) )
63 s1cli 
 |-  <" j "> e. Word _V
64 breq1 
 |-  ( f = <" j "> -> ( f ( Cycles ` G ) <" A A "> <-> <" j "> ( Cycles ` G ) <" A A "> ) )
65 fveqeq2 
 |-  ( f = <" j "> -> ( ( # ` f ) = 1 <-> ( # ` <" j "> ) = 1 ) )
66 64 65 3anbi12d 
 |-  ( f = <" j "> -> ( ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) <-> ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) ) )
67 66 rspcev 
 |-  ( ( <" j "> e. Word _V /\ ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) ) -> E. f e. Word _V ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) )
68 63 67 mpan 
 |-  ( ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) -> E. f e. Word _V ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) )
69 rexex 
 |-  ( E. f e. Word _V ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) -> E. f ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) )
70 68 69 syl 
 |-  ( ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) -> E. f ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) )
71 70 exlimiv 
 |-  ( E. j ( <" j "> ( Cycles ` G ) <" A A "> /\ ( # ` <" j "> ) = 1 /\ ( <" A A "> ` 0 ) = A ) -> E. f ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) )
72 62 71 syl 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> E. f ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) )
73 s2cli 
 |-  <" A A "> e. Word _V
74 breq2 
 |-  ( p = <" A A "> -> ( f ( Cycles ` G ) p <-> f ( Cycles ` G ) <" A A "> ) )
75 fveq1 
 |-  ( p = <" A A "> -> ( p ` 0 ) = ( <" A A "> ` 0 ) )
76 75 eqeq1d 
 |-  ( p = <" A A "> -> ( ( p ` 0 ) = A <-> ( <" A A "> ` 0 ) = A ) )
77 74 76 3anbi13d 
 |-  ( p = <" A A "> -> ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) <-> ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) ) )
78 77 rspcev 
 |-  ( ( <" A A "> e. Word _V /\ ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) ) -> E. p e. Word _V ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) )
79 73 78 mpan 
 |-  ( ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) -> E. p e. Word _V ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) )
80 rexex 
 |-  ( E. p e. Word _V ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) -> E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) )
81 79 80 syl 
 |-  ( ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) -> E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) )
82 81 eximi 
 |-  ( E. f ( f ( Cycles ` G ) <" A A "> /\ ( # ` f ) = 1 /\ ( <" A A "> ` 0 ) = A ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) )
83 72 82 syl 
 |-  ( ( G e. UHGraph /\ { A } e. ( Edg ` G ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) )
84 83 ex 
 |-  ( G e. UHGraph -> ( { A } e. ( Edg ` G ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) ) )
85 29 84 impbid 
 |-  ( G e. UHGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = A ) <-> { A } e. ( Edg ` G ) ) )