| Step | Hyp | Ref
| Expression |
| 1 | | cyclprop 29813 |
. . . . . . . . . . . . 13
⊢ (𝑓(Cycles‘𝐺)𝑝 → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))) |
| 2 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑓) =
1 → (𝑝‘(♯‘𝑓)) = (𝑝‘1)) |
| 3 | 2 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑓) =
1 → ((𝑝‘0) =
(𝑝‘(♯‘𝑓)) ↔ (𝑝‘0) = (𝑝‘1))) |
| 4 | 3 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑓) =
1 → ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓))) ↔ (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)))) |
| 5 | 4 | biimpd 229 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑓) =
1 → ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓))) → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)))) |
| 6 | 1, 5 | mpan9 506 |
. . . . . . . . . . . 12
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))) |
| 7 | | pthiswlk 29745 |
. . . . . . . . . . . . 13
⊢ (𝑓(Paths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝) |
| 8 | 7 | anim1i 615 |
. . . . . . . . . . . 12
⊢ ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))) |
| 9 | 6, 8 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))) |
| 10 | 9 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) ∧ (♯‘𝑓) = 1) → ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1)) |
| 11 | 10 | anabss3 675 |
. . . . . . . . 9
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1)) |
| 12 | | df-3an 1089 |
. . . . . . . . 9
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1) ↔ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1)) |
| 13 | 11, 12 | sylibr 234 |
. . . . . . . 8
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1)) |
| 14 | | 3ancomb 1099 |
. . . . . . . 8
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1) ↔ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) |
| 15 | 13, 14 | sylib 218 |
. . . . . . 7
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) |
| 16 | | wlkl1loop 29656 |
. . . . . . . . . 10
⊢ (((Fun
(iEdg‘𝐺) ∧ 𝑓(Walks‘𝐺)𝑝) ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → {(𝑝‘0)} ∈ (Edg‘𝐺)) |
| 17 | 16 | expl 457 |
. . . . . . . . 9
⊢ (Fun
(iEdg‘𝐺) →
((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
| 18 | | eqid 2737 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 19 | 18 | uhgrfun 29083 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
| 20 | 17, 19 | syl11 33 |
. . . . . . . 8
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
| 21 | 20 | 3impb 1115 |
. . . . . . 7
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1)) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
| 22 | 15, 21 | syl 17 |
. . . . . 6
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
| 23 | 22 | 3adant3 1133 |
. . . . 5
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺))) |
| 24 | | sneq 4636 |
. . . . . . 7
⊢ ((𝑝‘0) = 𝐴 → {(𝑝‘0)} = {𝐴}) |
| 25 | 24 | eleq1d 2826 |
. . . . . 6
⊢ ((𝑝‘0) = 𝐴 → ({(𝑝‘0)} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ (Edg‘𝐺))) |
| 26 | 25 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → ({(𝑝‘0)} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ (Edg‘𝐺))) |
| 27 | 23, 26 | sylibd 239 |
. . . 4
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {𝐴} ∈ (Edg‘𝐺))) |
| 28 | 27 | exlimivv 1932 |
. . 3
⊢
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {𝐴} ∈ (Edg‘𝐺))) |
| 29 | 28 | com12 32 |
. 2
⊢ (𝐺 ∈ UHGraph →
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → {𝐴} ∈ (Edg‘𝐺))) |
| 30 | | edgval 29066 |
. . . . . . . . . . . . . 14
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 31 | 30 | eleq2i 2833 |
. . . . . . . . . . . . 13
⊢ ({𝐴} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ ran (iEdg‘𝐺)) |
| 32 | | elrnrexdm 7109 |
. . . . . . . . . . . . . 14
⊢ (Fun
(iEdg‘𝐺) →
({𝐴} ∈ ran
(iEdg‘𝐺) →
∃𝑗 ∈ dom
(iEdg‘𝐺){𝐴} = ((iEdg‘𝐺)‘𝑗))) |
| 33 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴} = ((iEdg‘𝐺)‘𝑗) ↔ ((iEdg‘𝐺)‘𝑗) = {𝐴}) |
| 34 | 33 | rexbii 3094 |
. . . . . . . . . . . . . 14
⊢
(∃𝑗 ∈ dom
(iEdg‘𝐺){𝐴} = ((iEdg‘𝐺)‘𝑗) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴}) |
| 35 | 32, 34 | imbitrdi 251 |
. . . . . . . . . . . . 13
⊢ (Fun
(iEdg‘𝐺) →
({𝐴} ∈ ran
(iEdg‘𝐺) →
∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴})) |
| 36 | 31, 35 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (Fun
(iEdg‘𝐺) →
({𝐴} ∈
(Edg‘𝐺) →
∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴})) |
| 37 | 19, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴})) |
| 38 | | df-rex 3071 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴} ↔ ∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴})) |
| 39 | 37, 38 | imbitrdi 251 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}))) |
| 40 | 18 | lp1cycl 30171 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → 〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉) |
| 41 | 40 | 3expib 1123 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UHGraph → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → 〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
| 42 | 41 | eximdv 1917 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UHGraph →
(∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → ∃𝑗〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
| 43 | 39, 42 | syld 47 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
| 44 | | s1len 14644 |
. . . . . . . . . . 11
⊢
(♯‘〈“𝑗”〉) = 1 |
| 45 | 44 | ax-gen 1795 |
. . . . . . . . . 10
⊢
∀𝑗(♯‘〈“𝑗”〉) =
1 |
| 46 | | 19.29r 1874 |
. . . . . . . . . 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 406 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1)) |
| 50 | | uhgredgn0 29145 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → {𝐴} ∈ (𝒫 (Vtx‘𝐺) ∖
{∅})) |
| 51 | | eldifsni 4790 |
. . . . . . . . . . 11
⊢ ({𝐴} ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → {𝐴} ≠
∅) |
| 52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → {𝐴} ≠ ∅) |
| 53 | | snnzb 4718 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅) |
| 54 | 52, 53 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → 𝐴 ∈ V) |
| 55 | | s2fv0 14926 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(〈“𝐴𝐴”〉‘0) = 𝐴) |
| 56 | 54, 55 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → (〈“𝐴𝐴”〉‘0) = 𝐴) |
| 57 | 56 | alrimiv 1927 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∀𝑗(〈“𝐴𝐴”〉‘0) = 𝐴) |
| 58 | | 19.29r 1874 |
. . . . . . 7
⊢
((∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ ∀𝑗(〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑗((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 59 | 49, 57, 58 | syl2anc 584 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 60 | | df-3an 1089 |
. . . . . . 7
⊢
((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) ↔ ((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 61 | 60 | exbii 1848 |
. . . . . 6
⊢
(∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) ↔ ∃𝑗((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1) ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 62 | 59, 61 | sylibr 234 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 63 | | s1cli 14643 |
. . . . . . . 8
⊢
〈“𝑗”〉 ∈ Word V |
| 64 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑓 = 〈“𝑗”〉 → (𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ↔ 〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
| 65 | | fveqeq2 6915 |
. . . . . . . . . 10
⊢ (𝑓 = 〈“𝑗”〉 →
((♯‘𝑓) = 1
↔ (♯‘〈“𝑗”〉) = 1)) |
| 66 | 64, 65 | 3anbi12d 1439 |
. . . . . . . . 9
⊢ (𝑓 = 〈“𝑗”〉 → ((𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) ↔ (〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴))) |
| 67 | 66 | rspcev 3622 |
. . . . . . . 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 3076 |
. . . . . . 7
⊢
(∃𝑓 ∈
Word V(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 70 | 68, 69 | syl 17 |
. . . . . 6
⊢
((〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 71 | 70 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑗(〈“𝑗”〉(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧
(♯‘〈“𝑗”〉) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 72 | 62, 71 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴)) |
| 73 | | s2cli 14919 |
. . . . . . 7
⊢
〈“𝐴𝐴”〉 ∈ Word
V |
| 74 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑝 = 〈“𝐴𝐴”〉 → (𝑓(Cycles‘𝐺)𝑝 ↔ 𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉)) |
| 75 | | fveq1 6905 |
. . . . . . . . . 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 3622 |
. . . . . . 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 3076 |
. . . . . 6
⊢
(∃𝑝 ∈
Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → ∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
| 81 | 79, 80 | syl 17 |
. . . . 5
⊢ ((𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
| 82 | 81 | eximi 1835 |
. . . 4
⊢
(∃𝑓(𝑓(Cycles‘𝐺)〈“𝐴𝐴”〉 ∧ (♯‘𝑓) = 1 ∧ (〈“𝐴𝐴”〉‘0) = 𝐴) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
| 83 | 72, 82 | syl 17 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)) |
| 84 | 83 | ex 412 |
. 2
⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))) |
| 85 | 29, 84 | impbid 212 |
1
⊢ (𝐺 ∈ UHGraph →
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺))) |