Step |
Hyp |
Ref |
Expression |
1 |
|
prclisacycgr.1 |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ ) |
3 |
1 2
|
syl5eq |
⊢ ( ¬ 𝐺 ∈ V → 𝑉 = ∅ ) |
4 |
|
br0 |
⊢ ¬ 𝑓 ∅ 𝑝 |
5 |
|
df-cycls |
⊢ Cycles = ( 𝑔 ∈ V ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } ) |
6 |
5
|
relmptopab |
⊢ Rel ( Cycles ‘ 𝐺 ) |
7 |
|
cycliswlk |
⊢ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) |
8 |
|
df-br |
⊢ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ 〈 𝑓 , 𝑝 〉 ∈ ( Cycles ‘ 𝐺 ) ) |
9 |
|
df-br |
⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ 〈 𝑓 , 𝑝 〉 ∈ ( Walks ‘ 𝐺 ) ) |
10 |
7 8 9
|
3imtr3i |
⊢ ( 〈 𝑓 , 𝑝 〉 ∈ ( Cycles ‘ 𝐺 ) → 〈 𝑓 , 𝑝 〉 ∈ ( Walks ‘ 𝐺 ) ) |
11 |
6 10
|
relssi |
⊢ ( Cycles ‘ 𝐺 ) ⊆ ( Walks ‘ 𝐺 ) |
12 |
1
|
eqeq1i |
⊢ ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ ) |
13 |
|
g0wlk0 |
⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ ) |
14 |
12 13
|
sylbi |
⊢ ( 𝑉 = ∅ → ( Walks ‘ 𝐺 ) = ∅ ) |
15 |
11 14
|
sseqtrid |
⊢ ( 𝑉 = ∅ → ( Cycles ‘ 𝐺 ) ⊆ ∅ ) |
16 |
|
ss0 |
⊢ ( ( Cycles ‘ 𝐺 ) ⊆ ∅ → ( Cycles ‘ 𝐺 ) = ∅ ) |
17 |
|
breq |
⊢ ( ( Cycles ‘ 𝐺 ) = ∅ → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ 𝑓 ∅ 𝑝 ) ) |
18 |
17
|
notbid |
⊢ ( ( Cycles ‘ 𝐺 ) = ∅ → ( ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ¬ 𝑓 ∅ 𝑝 ) ) |
19 |
15 16 18
|
3syl |
⊢ ( 𝑉 = ∅ → ( ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ¬ 𝑓 ∅ 𝑝 ) ) |
20 |
4 19
|
mpbiri |
⊢ ( 𝑉 = ∅ → ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ) |
21 |
20
|
intnanrd |
⊢ ( 𝑉 = ∅ → ¬ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) |
22 |
21
|
nexdv |
⊢ ( 𝑉 = ∅ → ¬ ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) |
23 |
22
|
nexdv |
⊢ ( 𝑉 = ∅ → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) |
24 |
3 23
|
syl |
⊢ ( ¬ 𝐺 ∈ V → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) |