Proof of Theorem clwlknon2num
Step | Hyp | Ref
| Expression |
1 | | rusgrusgr 27438 |
. . . . . 6
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph) |
2 | | usgruspgr 27055 |
. . . . . 6
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
USPGraph) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph) |
4 | 3 | 3ad2ant2 1132 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝐺 ∈ USPGraph) |
5 | | clwlknon2num.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
6 | 5 | eleq2i 2842 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 ↔ 𝑋 ∈ (Vtx‘𝐺)) |
7 | 6 | biimpi 219 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (Vtx‘𝐺)) |
8 | 7 | 3ad2ant3 1133 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (Vtx‘𝐺)) |
9 | | 2nn 11732 |
. . . . 5
⊢ 2 ∈
ℕ |
10 | 9 | a1i 11 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 2 ∈ ℕ) |
11 | | clwwlknonclwlknonen 28232 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ (Vtx‘𝐺) ∧ 2 ∈ ℕ) →
{𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 2 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)2)) |
12 | 4, 8, 10, 11 | syl3anc 1369 |
. . 3
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)2)) |
13 | 1 | anim2i 620 |
. . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ∈ Fin ∧ 𝐺 ∈ USGraph)) |
14 | 13 | ancomd 466 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
15 | 5 | isfusgr 27192 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
16 | 14, 15 | sylibr 237 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph) |
17 | 16 | 3adant3 1130 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝐺 ∈ FinUSGraph) |
18 | | 2nn0 11936 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
19 | 18 | a1i 11 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → 2 ∈
ℕ0) |
20 | | wlksnfi 27777 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 2
∈ ℕ0) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = 2} ∈
Fin) |
21 | 17, 19, 20 | syl2anc 588 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = 2} ∈
Fin) |
22 | | clwlkswks 27649 |
. . . . . . 7
⊢
(ClWalks‘𝐺)
⊆ (Walks‘𝐺) |
23 | 22 | a1i 11 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (ClWalks‘𝐺) ⊆ (Walks‘𝐺)) |
24 | | simp2l 1197 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋) ∧ 𝑤 ∈ (ClWalks‘𝐺)) → (♯‘(1st
‘𝑤)) =
2) |
25 | 23, 24 | rabssrabd 3983 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ⊆ {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) =
2}) |
26 | 21, 25 | ssfid 8755 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ∈ Fin) |
27 | 5 | clwwlknonfin 27963 |
. . . . 5
⊢ (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)2) ∈ Fin) |
28 | 27 | 3ad2ant1 1131 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑋(ClWWalksNOn‘𝐺)2) ∈ Fin) |
29 | | hashen 13742 |
. . . 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 588 |
. . 3
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → ((♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)}) = (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) ↔ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)2))) |
31 | 12, 30 | mpbird 260 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)}) = (♯‘(𝑋(ClWWalksNOn‘𝐺)2))) |
32 | 7 | anim2i 620 |
. . . 4
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺))) |
33 | 32 | 3adant1 1128 |
. . 3
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺))) |
34 | | clwwlknon2num 27974 |
. . 3
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) = 𝐾) |
35 | 33, 34 | syl 17 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) = 𝐾) |
36 | 31, 35 | eqtrd 2794 |
1
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 2 ∧
((2nd ‘𝑤)‘0) = 𝑋)}) = 𝐾) |