Users' Mathboxes Mathbox for BTernaryTau < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  loop1cycl Structured version   Visualization version   GIF version

Theorem loop1cycl 34116
Description: A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023.)
Assertion
Ref Expression
loop1cycl (𝐺 ∈ UHGraph β†’ (βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) ↔ {𝐴} ∈ (Edgβ€˜πΊ)))
Distinct variable groups:   𝐺,𝑝   𝐴,𝑓,𝑝   𝑓,𝐺

Proof of Theorem loop1cycl
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 cyclprop 29039 . . . . . . . . . . . . 13 (𝑓(Cyclesβ€˜πΊ)𝑝 β†’ (𝑓(Pathsβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜(β™―β€˜π‘“))))
2 fveq2 6888 . . . . . . . . . . . . . . . 16 ((β™―β€˜π‘“) = 1 β†’ (π‘β€˜(β™―β€˜π‘“)) = (π‘β€˜1))
32eqeq2d 2743 . . . . . . . . . . . . . . 15 ((β™―β€˜π‘“) = 1 β†’ ((π‘β€˜0) = (π‘β€˜(β™―β€˜π‘“)) ↔ (π‘β€˜0) = (π‘β€˜1)))
43anbi2d 629 . . . . . . . . . . . . . 14 ((β™―β€˜π‘“) = 1 β†’ ((𝑓(Pathsβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜(β™―β€˜π‘“))) ↔ (𝑓(Pathsβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1))))
54biimpd 228 . . . . . . . . . . . . 13 ((β™―β€˜π‘“) = 1 β†’ ((𝑓(Pathsβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜(β™―β€˜π‘“))) β†’ (𝑓(Pathsβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1))))
61, 5mpan9 507 . . . . . . . . . . . 12 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1) β†’ (𝑓(Pathsβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1)))
7 pthiswlk 28973 . . . . . . . . . . . . 13 (𝑓(Pathsβ€˜πΊ)𝑝 β†’ 𝑓(Walksβ€˜πΊ)𝑝)
87anim1i 615 . . . . . . . . . . . 12 ((𝑓(Pathsβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1)) β†’ (𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1)))
96, 8syl 17 . . . . . . . . . . 11 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1) β†’ (𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1)))
109anim1i 615 . . . . . . . . . 10 (((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1) ∧ (β™―β€˜π‘“) = 1) β†’ ((𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1)) ∧ (β™―β€˜π‘“) = 1))
1110anabss3 673 . . . . . . . . 9 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1) β†’ ((𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1)) ∧ (β™―β€˜π‘“) = 1))
12 df-3an 1089 . . . . . . . . 9 ((𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1) ∧ (β™―β€˜π‘“) = 1) ↔ ((𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1)) ∧ (β™―β€˜π‘“) = 1))
1311, 12sylibr 233 . . . . . . . 8 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1) β†’ (𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1) ∧ (β™―β€˜π‘“) = 1))
14 3ancomb 1099 . . . . . . . 8 ((𝑓(Walksβ€˜πΊ)𝑝 ∧ (π‘β€˜0) = (π‘β€˜1) ∧ (β™―β€˜π‘“) = 1) ↔ (𝑓(Walksβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = (π‘β€˜1)))
1513, 14sylib 217 . . . . . . 7 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1) β†’ (𝑓(Walksβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = (π‘β€˜1)))
16 wlkl1loop 28884 . . . . . . . . . 10 (((Fun (iEdgβ€˜πΊ) ∧ 𝑓(Walksβ€˜πΊ)𝑝) ∧ ((β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = (π‘β€˜1))) β†’ {(π‘β€˜0)} ∈ (Edgβ€˜πΊ))
1716expl 458 . . . . . . . . 9 (Fun (iEdgβ€˜πΊ) β†’ ((𝑓(Walksβ€˜πΊ)𝑝 ∧ ((β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = (π‘β€˜1))) β†’ {(π‘β€˜0)} ∈ (Edgβ€˜πΊ)))
18 eqid 2732 . . . . . . . . . 10 (iEdgβ€˜πΊ) = (iEdgβ€˜πΊ)
1918uhgrfun 28315 . . . . . . . . 9 (𝐺 ∈ UHGraph β†’ Fun (iEdgβ€˜πΊ))
2017, 19syl11 33 . . . . . . . 8 ((𝑓(Walksβ€˜πΊ)𝑝 ∧ ((β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = (π‘β€˜1))) β†’ (𝐺 ∈ UHGraph β†’ {(π‘β€˜0)} ∈ (Edgβ€˜πΊ)))
21203impb 1115 . . . . . . 7 ((𝑓(Walksβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = (π‘β€˜1)) β†’ (𝐺 ∈ UHGraph β†’ {(π‘β€˜0)} ∈ (Edgβ€˜πΊ)))
2215, 21syl 17 . . . . . 6 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1) β†’ (𝐺 ∈ UHGraph β†’ {(π‘β€˜0)} ∈ (Edgβ€˜πΊ)))
23223adant3 1132 . . . . 5 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) β†’ (𝐺 ∈ UHGraph β†’ {(π‘β€˜0)} ∈ (Edgβ€˜πΊ)))
24 sneq 4637 . . . . . . 7 ((π‘β€˜0) = 𝐴 β†’ {(π‘β€˜0)} = {𝐴})
2524eleq1d 2818 . . . . . 6 ((π‘β€˜0) = 𝐴 β†’ ({(π‘β€˜0)} ∈ (Edgβ€˜πΊ) ↔ {𝐴} ∈ (Edgβ€˜πΊ)))
26253ad2ant3 1135 . . . . 5 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) β†’ ({(π‘β€˜0)} ∈ (Edgβ€˜πΊ) ↔ {𝐴} ∈ (Edgβ€˜πΊ)))
2723, 26sylibd 238 . . . 4 ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) β†’ (𝐺 ∈ UHGraph β†’ {𝐴} ∈ (Edgβ€˜πΊ)))
2827exlimivv 1935 . . 3 (βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) β†’ (𝐺 ∈ UHGraph β†’ {𝐴} ∈ (Edgβ€˜πΊ)))
2928com12 32 . 2 (𝐺 ∈ UHGraph β†’ (βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) β†’ {𝐴} ∈ (Edgβ€˜πΊ)))
30 edgval 28298 . . . . . . . . . . . . . 14 (Edgβ€˜πΊ) = ran (iEdgβ€˜πΊ)
3130eleq2i 2825 . . . . . . . . . . . . 13 ({𝐴} ∈ (Edgβ€˜πΊ) ↔ {𝐴} ∈ ran (iEdgβ€˜πΊ))
32 elrnrexdm 7087 . . . . . . . . . . . . . 14 (Fun (iEdgβ€˜πΊ) β†’ ({𝐴} ∈ ran (iEdgβ€˜πΊ) β†’ βˆƒπ‘— ∈ dom (iEdgβ€˜πΊ){𝐴} = ((iEdgβ€˜πΊ)β€˜π‘—)))
33 eqcom 2739 . . . . . . . . . . . . . . 15 ({𝐴} = ((iEdgβ€˜πΊ)β€˜π‘—) ↔ ((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴})
3433rexbii 3094 . . . . . . . . . . . . . 14 (βˆƒπ‘— ∈ dom (iEdgβ€˜πΊ){𝐴} = ((iEdgβ€˜πΊ)β€˜π‘—) ↔ βˆƒπ‘— ∈ dom (iEdgβ€˜πΊ)((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴})
3532, 34imbitrdi 250 . . . . . . . . . . . . 13 (Fun (iEdgβ€˜πΊ) β†’ ({𝐴} ∈ ran (iEdgβ€˜πΊ) β†’ βˆƒπ‘— ∈ dom (iEdgβ€˜πΊ)((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴}))
3631, 35biimtrid 241 . . . . . . . . . . . 12 (Fun (iEdgβ€˜πΊ) β†’ ({𝐴} ∈ (Edgβ€˜πΊ) β†’ βˆƒπ‘— ∈ dom (iEdgβ€˜πΊ)((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴}))
3719, 36syl 17 . . . . . . . . . . 11 (𝐺 ∈ UHGraph β†’ ({𝐴} ∈ (Edgβ€˜πΊ) β†’ βˆƒπ‘— ∈ dom (iEdgβ€˜πΊ)((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴}))
38 df-rex 3071 . . . . . . . . . . 11 (βˆƒπ‘— ∈ dom (iEdgβ€˜πΊ)((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴} ↔ βˆƒπ‘—(𝑗 ∈ dom (iEdgβ€˜πΊ) ∧ ((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴}))
3937, 38imbitrdi 250 . . . . . . . . . 10 (𝐺 ∈ UHGraph β†’ ({𝐴} ∈ (Edgβ€˜πΊ) β†’ βˆƒπ‘—(𝑗 ∈ dom (iEdgβ€˜πΊ) ∧ ((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴})))
4018lp1cycl 29394 . . . . . . . . . . . 12 ((𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom (iEdgβ€˜πΊ) ∧ ((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴}) β†’ βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ©)
41403expib 1122 . . . . . . . . . . 11 (𝐺 ∈ UHGraph β†’ ((𝑗 ∈ dom (iEdgβ€˜πΊ) ∧ ((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴}) β†’ βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ©))
4241eximdv 1920 . . . . . . . . . 10 (𝐺 ∈ UHGraph β†’ (βˆƒπ‘—(𝑗 ∈ dom (iEdgβ€˜πΊ) ∧ ((iEdgβ€˜πΊ)β€˜π‘—) = {𝐴}) β†’ βˆƒπ‘—βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ©))
4339, 42syld 47 . . . . . . . . 9 (𝐺 ∈ UHGraph β†’ ({𝐴} ∈ (Edgβ€˜πΊ) β†’ βˆƒπ‘—βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ©))
44 s1len 14552 . . . . . . . . . . 11 (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1
4544ax-gen 1797 . . . . . . . . . 10 βˆ€π‘—(β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1
46 19.29r 1877 . . . . . . . . . 10 ((βˆƒπ‘—βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ βˆ€π‘—(β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1) β†’ βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1))
4745, 46mpan2 689 . . . . . . . . 9 (βˆƒπ‘—βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© β†’ βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1))
4843, 47syl6 35 . . . . . . . 8 (𝐺 ∈ UHGraph β†’ ({𝐴} ∈ (Edgβ€˜πΊ) β†’ βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1)))
4948imp 407 . . . . . . 7 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1))
50 uhgredgn0 28377 . . . . . . . . . . 11 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ {𝐴} ∈ (𝒫 (Vtxβ€˜πΊ) βˆ– {βˆ…}))
51 eldifsni 4792 . . . . . . . . . . 11 ({𝐴} ∈ (𝒫 (Vtxβ€˜πΊ) βˆ– {βˆ…}) β†’ {𝐴} β‰  βˆ…)
5250, 51syl 17 . . . . . . . . . 10 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ {𝐴} β‰  βˆ…)
53 snnzb 4721 . . . . . . . . . 10 (𝐴 ∈ V ↔ {𝐴} β‰  βˆ…)
5452, 53sylibr 233 . . . . . . . . 9 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ 𝐴 ∈ V)
55 s2fv0 14834 . . . . . . . . 9 (𝐴 ∈ V β†’ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴)
5654, 55syl 17 . . . . . . . 8 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴)
5756alrimiv 1930 . . . . . . 7 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ βˆ€π‘—(βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴)
58 19.29r 1877 . . . . . . 7 ((βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1) ∧ βˆ€π‘—(βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘—((βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1) ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
5949, 57, 58syl2anc 584 . . . . . 6 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ βˆƒπ‘—((βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1) ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
60 df-3an 1089 . . . . . . 7 ((βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) ↔ ((βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1) ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
6160exbii 1850 . . . . . 6 (βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) ↔ βˆƒπ‘—((βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1) ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
6259, 61sylibr 233 . . . . 5 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
63 s1cli 14551 . . . . . . . 8 βŸ¨β€œπ‘—β€βŸ© ∈ Word V
64 breq1 5150 . . . . . . . . . 10 (𝑓 = βŸ¨β€œπ‘—β€βŸ© β†’ (𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ↔ βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ©))
65 fveqeq2 6897 . . . . . . . . . 10 (𝑓 = βŸ¨β€œπ‘—β€βŸ© β†’ ((β™―β€˜π‘“) = 1 ↔ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1))
6664, 653anbi12d 1437 . . . . . . . . 9 (𝑓 = βŸ¨β€œπ‘—β€βŸ© β†’ ((𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) ↔ (βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴)))
6766rspcev 3612 . . . . . . . 8 ((βŸ¨β€œπ‘—β€βŸ© ∈ Word V ∧ (βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴)) β†’ βˆƒπ‘“ ∈ Word V(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
6863, 67mpan 688 . . . . . . 7 ((βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘“ ∈ Word V(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
69 rexex 3076 . . . . . . 7 (βˆƒπ‘“ ∈ Word V(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘“(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
7068, 69syl 17 . . . . . 6 ((βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘“(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
7170exlimiv 1933 . . . . 5 (βˆƒπ‘—(βŸ¨β€œπ‘—β€βŸ©(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜βŸ¨β€œπ‘—β€βŸ©) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘“(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
7262, 71syl 17 . . . 4 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ βˆƒπ‘“(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
73 s2cli 14827 . . . . . . 7 βŸ¨β€œπ΄π΄β€βŸ© ∈ Word V
74 breq2 5151 . . . . . . . . 9 (𝑝 = βŸ¨β€œπ΄π΄β€βŸ© β†’ (𝑓(Cyclesβ€˜πΊ)𝑝 ↔ 𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ©))
75 fveq1 6887 . . . . . . . . . 10 (𝑝 = βŸ¨β€œπ΄π΄β€βŸ© β†’ (π‘β€˜0) = (βŸ¨β€œπ΄π΄β€βŸ©β€˜0))
7675eqeq1d 2734 . . . . . . . . 9 (𝑝 = βŸ¨β€œπ΄π΄β€βŸ© β†’ ((π‘β€˜0) = 𝐴 ↔ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴))
7774, 763anbi13d 1438 . . . . . . . 8 (𝑝 = βŸ¨β€œπ΄π΄β€βŸ© β†’ ((𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) ↔ (𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴)))
7877rspcev 3612 . . . . . . 7 ((βŸ¨β€œπ΄π΄β€βŸ© ∈ Word V ∧ (𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴)) β†’ βˆƒπ‘ ∈ Word V(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴))
7973, 78mpan 688 . . . . . 6 ((𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘ ∈ Word V(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴))
80 rexex 3076 . . . . . 6 (βˆƒπ‘ ∈ Word V(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) β†’ βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴))
8179, 80syl 17 . . . . 5 ((𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴))
8281eximi 1837 . . . 4 (βˆƒπ‘“(𝑓(Cyclesβ€˜πΊ)βŸ¨β€œπ΄π΄β€βŸ© ∧ (β™―β€˜π‘“) = 1 ∧ (βŸ¨β€œπ΄π΄β€βŸ©β€˜0) = 𝐴) β†’ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴))
8372, 82syl 17 . . 3 ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edgβ€˜πΊ)) β†’ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴))
8483ex 413 . 2 (𝐺 ∈ UHGraph β†’ ({𝐴} ∈ (Edgβ€˜πΊ) β†’ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴)))
8529, 84impbid 211 1 (𝐺 ∈ UHGraph β†’ (βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜πΊ)𝑝 ∧ (β™―β€˜π‘“) = 1 ∧ (π‘β€˜0) = 𝐴) ↔ {𝐴} ∈ (Edgβ€˜πΊ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆƒwrex 3070  Vcvv 3474   βˆ– cdif 3944  βˆ…c0 4321  π’« cpw 4601  {csn 4627   class class class wbr 5147  dom cdm 5675  ran crn 5676  Fun wfun 6534  β€˜cfv 6540  0cc0 11106  1c1 11107  β™―chash 14286  Word cword 14460  βŸ¨β€œcs1 14541  βŸ¨β€œcs2 14788  Vtxcvtx 28245  iEdgciedg 28246  Edgcedg 28296  UHGraphcuhgr 28305  Walkscwlks 28842  Pathscpths 28958  Cyclesccycls 29031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ifp 1062  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-fzo 13624  df-hash 14287  df-word 14461  df-concat 14517  df-s1 14542  df-s2 14795  df-edg 28297  df-uhgr 28307  df-wlks 28845  df-wlkson 28846  df-trls 28938  df-trlson 28939  df-pths 28962  df-pthson 28964  df-cycls 29033
This theorem is referenced by:  acycgrislfgr  34131
  Copyright terms: Public domain W3C validator