Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( ClWWalks ‘ 𝑔 ) = ( ClWWalks ‘ 𝐺 ) ) |
2 |
1
|
adantl |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ClWWalks ‘ 𝑔 ) = ( ClWWalks ‘ 𝐺 ) ) |
3 |
|
eqeq2 |
⊢ ( 𝑛 = 𝑁 → ( ( ♯ ‘ 𝑤 ) = 𝑛 ↔ ( ♯ ‘ 𝑤 ) = 𝑁 ) ) |
4 |
3
|
adantr |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = 𝑛 ↔ ( ♯ ‘ 𝑤 ) = 𝑁 ) ) |
5 |
2 4
|
rabeqbidv |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) |
6 |
|
df-clwwlkn |
⊢ ClWWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } ) |
7 |
|
fvex |
⊢ ( ClWWalks ‘ 𝐺 ) ∈ V |
8 |
7
|
rabex |
⊢ { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ V |
9 |
5 6 8
|
ovmpoa |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) |
10 |
6
|
mpondm0 |
⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ ) |
11 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
12 |
11
|
clwwlkbp |
⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑤 ≠ ∅ ) ) |
13 |
12
|
simp2d |
⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) |
14 |
|
lencl |
⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 ) |
15 |
13 14
|
syl |
⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 ) |
16 |
|
eleq1 |
⊢ ( ( ♯ ‘ 𝑤 ) = 𝑁 → ( ( ♯ ‘ 𝑤 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) ) |
17 |
15 16
|
syl5ibcom |
⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = 𝑁 → 𝑁 ∈ ℕ0 ) ) |
18 |
17
|
con3rr3 |
⊢ ( ¬ 𝑁 ∈ ℕ0 → ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) ) |
19 |
18
|
ralrimiv |
⊢ ( ¬ 𝑁 ∈ ℕ0 → ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) |
20 |
|
ral0 |
⊢ ∀ 𝑤 ∈ ∅ ¬ ( ♯ ‘ 𝑤 ) = 𝑁 |
21 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( ClWWalks ‘ 𝐺 ) = ∅ ) |
22 |
21
|
raleqdv |
⊢ ( ¬ 𝐺 ∈ V → ( ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ↔ ∀ 𝑤 ∈ ∅ ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) ) |
23 |
20 22
|
mpbiri |
⊢ ( ¬ 𝐺 ∈ V → ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) |
24 |
19 23
|
jaoi |
⊢ ( ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝐺 ∈ V ) → ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) |
25 |
|
ianor |
⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ↔ ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝐺 ∈ V ) ) |
26 |
|
rabeq0 |
⊢ ( { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ∅ ↔ ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 𝑁 ) |
27 |
24 25 26
|
3imtr4i |
⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ∅ ) |
28 |
10 27
|
eqtr4d |
⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) |
29 |
9 28
|
pm2.61i |
⊢ ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } |