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