Step | Hyp | Ref
| Expression |
1 | | cyclprop 27880 |
. . . . . . . . . . . . 13
⊢ (𝑓(Cycles‘𝐺)𝑝 → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))) |
2 | | fveq2 6717 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑓) =
1 → (𝑝‘(♯‘𝑓)) = (𝑝‘1)) |
3 | 2 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑓) =
1 → ((𝑝‘0) =
(𝑝‘(♯‘𝑓)) ↔ (𝑝‘0) = (𝑝‘1))) |
4 | 3 | anbi2d 632 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑓) =
1 → ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓))) ↔ (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)))) |
5 | 4 | biimpd 232 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑓) =
1 → ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓))) → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)))) |
6 | 1, 5 | mpan9 510 |
. . . . . . . . . . . 12
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))) |
7 | | pthiswlk 27814 |
. . . . . . . . . . . . 13
⊢ (𝑓(Paths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝) |
8 | 7 | anim1i 618 |
. . . . . . . . . . . 12
⊢ ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))) |
9 | 6, 8 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))) |
10 | 9 | anim1i 618 |
. . . . . . . . . 10
⊢ (((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) ∧ (♯‘𝑓) = 1) → ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1)) |
11 | 10 | anabss3 675 |
. . . . . . . . 9
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1)) |
12 | | df-3an 1091 |
. . . . . . . . 9
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1) ↔ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1)) |
13 | 11, 12 | sylibr 237 |
. . . . . . . 8
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1)) |
14 | | 3ancomb 1101 |
. . . . . . . 8
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1) ↔ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) |
15 | 13, 14 | sylib 221 |
. . . . . . 7
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) |
16 | | wlkl1loop 27725 |
. . . . . . . . . 10
⊢ (((Fun
(iEdg‘𝐺) ∧ 𝑓(Walks‘𝐺)𝑝) ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → {(𝑝‘0)} ∈ (Edg‘𝐺)) |
17 | 16 | expl 461 |
. . . . . . . . 9
⊢ (Fun
(iEdg‘𝐺) →
((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
18 | | eqid 2737 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
19 | 18 | uhgrfun 27157 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
20 | 17, 19 | syl11 33 |
. . . . . . . 8
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
21 | 20 | 3impb 1117 |
. . . . . . 7
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1)) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
22 | 15, 21 | syl 17 |
. . . . . 6
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
23 | 22 | 3adant3 1134 |
. . . . 5
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
24 | | sneq 4551 |
. . . . . . 7
⊢ ((𝑝‘0) = 𝐴 → {(𝑝‘0)} = {𝐴}) |
25 | 24 | eleq1d 2822 |
. . . . . 6
⊢ ((𝑝‘0) = 𝐴 → ({(𝑝‘0)} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ (Edg‘𝐺))) |
26 | 25 | 3ad2ant3 1137 |
. . . . 5
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → ({(𝑝‘0)} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ (Edg‘𝐺))) |
27 | 23, 26 | sylibd 242 |
. . . 4
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {𝐴} ∈ (Edg‘𝐺))) |
28 | 27 | exlimivv 1940 |
. . 3
⊢
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {𝐴} ∈ (Edg‘𝐺))) |
29 | 28 | com12 32 |
. 2
⊢ (𝐺 ∈ UHGraph →
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → {𝐴} ∈ (Edg‘𝐺))) |
30 | | edgval 27140 |
. . . . . . . . . . . . . 14
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
31 | 30 | eleq2i 2829 |
. . . . . . . . . . . . 13
⊢ ({𝐴} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ ran (iEdg‘𝐺)) |
32 | | elrnrexdm 6908 |
. . . . . . . . . . . . . 14
⊢ (Fun
(iEdg‘𝐺) →
({𝐴} ∈ ran
(iEdg‘𝐺) →
∃𝑗 ∈ dom
(iEdg‘𝐺){𝐴} = ((iEdg‘𝐺)‘𝑗))) |
33 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴} = ((iEdg‘𝐺)‘𝑗) ↔ ((iEdg‘𝐺)‘𝑗) = {𝐴}) |
34 | 33 | rexbii 3170 |
. . . . . . . . . . . . . 14
⊢
(∃𝑗 ∈ dom
(iEdg‘𝐺){𝐴} = ((iEdg‘𝐺)‘𝑗) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴}) |
35 | 32, 34 | syl6ib 254 |
. . . . . . . . . . . . 13
⊢ (Fun
(iEdg‘𝐺) →
({𝐴} ∈ ran
(iEdg‘𝐺) →
∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴})) |
36 | 31, 35 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ (Fun
(iEdg‘𝐺) →
({𝐴} ∈
(Edg‘𝐺) →
∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴})) |
37 | 19, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴})) |
38 | | df-rex 3067 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴} ↔ ∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴})) |
39 | 37, 38 | syl6ib 254 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}))) |
40 | 18 | lp1cycl 28235 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → 〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉) |
41 | 40 | 3expib 1124 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UHGraph → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → 〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
42 | 41 | eximdv 1925 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UHGraph →
(∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → ∃𝑗〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
43 | 39, 42 | syld 47 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
44 | | s1len 14163 |
. . . . . . . . . . 11
⊢
(♯‘〈“𝑗”〉) = 1 |
45 | 44 | ax-gen 1803 |
. . . . . . . . . 10
⊢
∀𝑗(♯‘〈“𝑗”〉) =
1 |
46 | | 19.29r 1882 |
. . . . . . . . . 10
⊢
((∃𝑗〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ ∀𝑗(♯‘〈“𝑗”〉) = 1) →
∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1)) |
47 | 45, 46 | mpan2 691 |
. . . . . . . . 9
⊢
(∃𝑗〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 → ∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1)) |
48 | 43, 47 | syl6 35 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1))) |
49 | 48 | imp 410 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1)) |
50 | | uhgredgn0 27219 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → {𝐴} ∈ (𝒫 (Vtx‘𝐺) ∖
{∅})) |
51 | | eldifsni 4703 |
. . . . . . . . . . 11
⊢ ({𝐴} ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → {𝐴} ≠
∅) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → {𝐴} ≠ ∅) |
53 | | snnzb 4634 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅) |
54 | 52, 53 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → 𝐴 ∈ V) |
55 | | s2fv0 14452 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(〈“𝐴𝐴”〉‘0) = 𝐴) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → (〈“𝐴𝐴”〉‘0) = 𝐴) |
57 | 56 | alrimiv 1935 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∀𝑗(〈“𝐴𝐴”〉‘0) = 𝐴) |
58 | | 19.29r 1882 |
. . . . . . 7
⊢
((∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ ∀𝑗(〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑗((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
59 | 49, 57, 58 | syl2anc 587 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
60 | | df-3an 1091 |
. . . . . . 7
⊢
((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) ↔ ((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
61 | 60 | exbii 1855 |
. . . . . 6
⊢
(∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) ↔ ∃𝑗((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
62 | 59, 61 | sylibr 237 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
63 | | s1cli 14162 |
. . . . . . . 8
⊢
〈“𝑗”〉 ∈ Word V |
64 | | breq1 5056 |
. . . . . . . . . 10
⊢ (𝑓 = 〈“𝑗”〉 → (𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ↔ 〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
65 | | fveqeq2 6726 |
. . . . . . . . . 10
⊢ (𝑓 = 〈“𝑗”〉 →
((♯‘𝑓) = 1
↔ (♯‘〈“𝑗”〉) = 1)) |
66 | 64, 65 | 3anbi12d 1439 |
. . . . . . . . 9
⊢ (𝑓 = 〈“𝑗”〉 → ((𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) ↔ (〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴))) |
67 | 66 | rspcev 3537 |
. . . . . . . 8
⊢
((〈“𝑗”〉 ∈ Word V ∧
(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) → ∃𝑓 ∈ Word V(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
68 | 63, 67 | mpan 690 |
. . . . . . 7
⊢
((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓 ∈ Word V(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
69 | | rexex 3162 |
. . . . . . 7
⊢
(∃𝑓 ∈
Word V(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
70 | 68, 69 | syl 17 |
. . . . . 6
⊢
((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
71 | 70 | exlimiv 1938 |
. . . . 5
⊢
(∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
72 | 62, 71 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
73 | | s2cli 14445 |
. . . . . . 7
⊢
〈“𝐴𝐴”〉 ∈ Word
V |
74 | | breq2 5057 |
. . . . . . . . 9
⊢ (𝑝 = 〈“𝐴𝐴”〉 → (𝑓(Cycles‘𝐺)𝑝 ↔ 𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
75 | | fveq1 6716 |
. . . . . . . . . 10
⊢ (𝑝 = 〈“𝐴𝐴”〉 → (𝑝‘0) = (〈“𝐴𝐴”〉‘0)) |
76 | 75 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑝 = 〈“𝐴𝐴”〉 → ((𝑝‘0) = 𝐴 ↔ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
77 | 74, 76 | 3anbi13d 1440 |
. . . . . . . 8
⊢ (𝑝 = 〈“𝐴𝐴”〉 → ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ (𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴))) |
78 | 77 | rspcev 3537 |
. . . . . . 7
⊢
((〈“𝐴𝐴”〉 ∈ Word V ∧ (𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) → ∃𝑝 ∈ Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
79 | 73, 78 | mpan 690 |
. . . . . 6
⊢ ((𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑝 ∈ Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
80 | | rexex 3162 |
. . . . . 6
⊢
(∃𝑝 ∈
Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → ∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
81 | 79, 80 | syl 17 |
. . . . 5
⊢ ((𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
82 | 81 | eximi 1842 |
. . . 4
⊢
(∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
83 | 72, 82 | syl 17 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
84 | 83 | ex 416 |
. 2
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))) |
85 | 29, 84 | impbid 215 |
1
⊢ (𝐺 ∈ UHGraph →
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺))) |