Proof of Theorem clwlknon2num
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rusgrusgr 29583 | . . . . . 6
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph) | 
| 2 |  | usgruspgr 29198 | . . . . . 6
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
USPGraph) | 
| 3 | 1, 2 | syl 17 | . . . . 5
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph) | 
| 4 | 3 | 3ad2ant2 1134 | . . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝐺 ∈ USPGraph) | 
| 5 |  | clwlknon2num.v | . . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) | 
| 6 | 5 | eleq2i 2832 | . . . . . 6
⊢ (𝑋 ∈ 𝑉 ↔ 𝑋 ∈ (Vtx‘𝐺)) | 
| 7 | 6 | biimpi 216 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (Vtx‘𝐺)) | 
| 8 | 7 | 3ad2ant3 1135 | . . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (Vtx‘𝐺)) | 
| 9 |  | 2nn 12340 | . . . . 5
⊢ 2 ∈
ℕ | 
| 10 | 9 | a1i 11 | . . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 2 ∈ ℕ) | 
| 11 |  | clwwlknonclwlknonen 30383 | . . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ (Vtx‘𝐺) ∧ 2 ∈ ℕ) →
{𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 2 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)2)) | 
| 12 | 4, 8, 10, 11 | syl3anc 1372 | . . 3
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)2)) | 
| 13 | 1 | anim2i 617 | . . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ∈ Fin ∧ 𝐺 ∈ USGraph)) | 
| 14 | 13 | ancomd 461 | . . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) | 
| 15 | 5 | isfusgr 29336 | . . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) | 
| 16 | 14, 15 | sylibr 234 | . . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph) | 
| 17 | 16 | 3adant3 1132 | . . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝐺 ∈ FinUSGraph) | 
| 18 |  | 2nn0 12545 | . . . . . . 7
⊢ 2 ∈
ℕ0 | 
| 19 | 18 | a1i 11 | . . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 2 ∈
ℕ0) | 
| 20 |  | wlksnfi 29928 | . . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 2
∈ ℕ0) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = 2} ∈
Fin) | 
| 21 | 17, 19, 20 | syl2anc 584 | . . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = 2} ∈
Fin) | 
| 22 |  | clwlkswks 29797 | . . . . . . 7
⊢
(ClWalks‘𝐺)
⊆ (Walks‘𝐺) | 
| 23 | 22 | a1i 11 | . . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (ClWalks‘𝐺) ⊆ (Walks‘𝐺)) | 
| 24 |  | simp2l 1199 | . . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋) ∧ 𝑤 ∈ (ClWalks‘𝐺)) → (♯‘(1st
‘𝑤)) =
2) | 
| 25 | 23, 24 | rabssrabd 4082 | . . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ⊆ {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) =
2}) | 
| 26 | 21, 25 | ssfid 9302 | . . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ∈ Fin) | 
| 27 | 5 | clwwlknonfin 30114 | . . . . 5
⊢ (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)2) ∈ Fin) | 
| 28 | 27 | 3ad2ant1 1133 | . . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑋(ClWWalksNOn‘𝐺)2) ∈ Fin) | 
| 29 |  | hashen 14387 | . . . 4
⊢ (({𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 2 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ∈ Fin ∧ (𝑋(ClWWalksNOn‘𝐺)2) ∈ Fin) →
((♯‘{𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 2 ∧ ((2nd ‘𝑤)‘0) = 𝑋)}) = (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) ↔ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)2))) | 
| 30 | 26, 28, 29 | syl2anc 584 | . . 3
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → ((♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)}) = (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) ↔ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)2))) | 
| 31 | 12, 30 | mpbird 257 | . 2
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)}) = (♯‘(𝑋(ClWWalksNOn‘𝐺)2))) | 
| 32 | 7 | anim2i 617 | . . . 4
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺))) | 
| 33 | 32 | 3adant1 1130 | . . 3
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺))) | 
| 34 |  | clwwlknon2num 30125 | . . 3
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) = 𝐾) | 
| 35 | 33, 34 | syl 17 | . 2
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) = 𝐾) | 
| 36 | 31, 35 | eqtrd 2776 | 1
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)}) = 𝐾) |