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 UHGraph f p f Cycles G p f = 1 p 0 = A A 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 Edg G
17 16 expl Fun iEdg G f Walks G p f = 1 p 0 = p 1 p 0 Edg G
18 eqid iEdg G = iEdg G
19 18 uhgrfun G UHGraph Fun iEdg G
20 17 19 syl11 f Walks G p f = 1 p 0 = p 1 G UHGraph p 0 Edg G
21 20 3impb f Walks G p f = 1 p 0 = p 1 G UHGraph p 0 Edg G
22 15 21 syl f Cycles G p f = 1 G UHGraph p 0 Edg G
23 22 3adant3 f Cycles G p f = 1 p 0 = A G UHGraph p 0 Edg G
24 sneq p 0 = A p 0 = A
25 24 eleq1d p 0 = A p 0 Edg G A Edg G
26 25 3ad2ant3 f Cycles G p f = 1 p 0 = A p 0 Edg G A Edg G
27 23 26 sylibd f Cycles G p f = 1 p 0 = A G UHGraph A Edg G
28 27 exlimivv f p f Cycles G p f = 1 p 0 = A G UHGraph A Edg G
29 28 com12 G UHGraph f p f Cycles G p f = 1 p 0 = A A Edg G
30 edgval Edg G = ran iEdg G
31 30 eleq2i A Edg G A ran iEdg G
32 elrnrexdm Fun iEdg G A ran iEdg G j dom iEdg G A = iEdg G j
33 eqcom A = iEdg G j iEdg G j = A
34 33 rexbii j dom iEdg G A = iEdg G j j dom iEdg G iEdg G j = A
35 32 34 syl6ib Fun iEdg G A ran iEdg G j dom iEdg G iEdg G j = A
36 31 35 syl5bi Fun iEdg G A Edg G j dom iEdg G iEdg G j = A
37 19 36 syl G UHGraph A Edg G j dom iEdg G iEdg G j = A
38 df-rex j dom iEdg G iEdg G j = A j j dom iEdg G iEdg G j = A
39 37 38 syl6ib G UHGraph A Edg G j j dom iEdg G iEdg G j = A
40 18 lp1cycl G UHGraph j dom iEdg G iEdg G j = A ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩
41 40 3expib G UHGraph j dom iEdg G iEdg G j = A ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩
42 41 eximdv G UHGraph j j dom iEdg G iEdg G j = A j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩
43 39 42 syld G UHGraph A Edg G j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩
44 s1len ⟨“ j ”⟩ = 1
45 44 ax-gen j ⟨“ j ”⟩ = 1
46 19.29r j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ j ⟨“ j ”⟩ = 1 j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1
47 45 46 mpan2 j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1
48 43 47 syl6 G UHGraph A Edg G j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1
49 48 imp G UHGraph A Edg G j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1
50 uhgredgn0 G UHGraph A Edg G A 𝒫 Vtx G
51 eldifsni A 𝒫 Vtx G A
52 50 51 syl G UHGraph A Edg G A
53 snnzb A V A
54 52 53 sylibr G UHGraph A Edg G A V
55 s2fv0 A V ⟨“ AA ”⟩ 0 = A
56 54 55 syl G UHGraph A Edg G ⟨“ AA ”⟩ 0 = A
57 56 alrimiv G UHGraph A Edg G j ⟨“ AA ”⟩ 0 = A
58 19.29r j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 j ⟨“ AA ”⟩ 0 = A j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A
59 49 57 58 syl2anc G UHGraph A Edg G j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A
60 df-3an ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A
61 60 exbii j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A
62 59 61 sylibr G UHGraph A Edg G j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A
63 s1cli ⟨“ j ”⟩ Word V
64 breq1 f = ⟨“ j ”⟩ f Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩
65 fveqeq2 f = ⟨“ j ”⟩ f = 1 ⟨“ j ”⟩ = 1
66 64 65 3anbi12d f = ⟨“ j ”⟩ f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A
67 66 rspcev ⟨“ j ”⟩ Word V ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A f Word V f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A
68 63 67 mpan ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A f Word V f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A
69 rexex f Word V f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A f f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A
70 68 69 syl ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A f f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A
71 70 exlimiv j ⟨“ j ”⟩ Cycles G ⟨“ AA ”⟩ ⟨“ j ”⟩ = 1 ⟨“ AA ”⟩ 0 = A f f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A
72 62 71 syl G UHGraph A Edg G f f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A
73 s2cli ⟨“ AA ”⟩ Word V
74 breq2 p = ⟨“ AA ”⟩ f Cycles G p f Cycles G ⟨“ AA ”⟩
75 fveq1 p = ⟨“ AA ”⟩ p 0 = ⟨“ AA ”⟩ 0
76 75 eqeq1d p = ⟨“ AA ”⟩ p 0 = A ⟨“ AA ”⟩ 0 = A
77 74 76 3anbi13d p = ⟨“ AA ”⟩ f Cycles G p f = 1 p 0 = A f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A
78 77 rspcev ⟨“ AA ”⟩ Word V f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A p Word V f Cycles G p f = 1 p 0 = A
79 73 78 mpan f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A p Word V f Cycles G p f = 1 p 0 = A
80 rexex p Word V f Cycles G p f = 1 p 0 = A p f Cycles G p f = 1 p 0 = A
81 79 80 syl f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A p f Cycles G p f = 1 p 0 = A
82 81 eximi f f Cycles G ⟨“ AA ”⟩ f = 1 ⟨“ AA ”⟩ 0 = A f p f Cycles G p f = 1 p 0 = A
83 72 82 syl G UHGraph A Edg G f p f Cycles G p f = 1 p 0 = A
84 83 ex G UHGraph A Edg G f p f Cycles G p f = 1 p 0 = A
85 29 84 impbid G UHGraph f p f Cycles G p f = 1 p 0 = A A Edg G