Proof of Theorem numclwwlk3lem2
| Step | Hyp | Ref
| Expression |
| 1 | | numclwwlk3lem2.c |
. . . . 5
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) |
| 2 | | numclwwlk3lem2.h |
. . . . 5
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣}) |
| 3 | 1, 2 | numclwwlk3lem2lem 30402 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋(ClWWalksNOn‘𝐺)𝑁) = ((𝑋𝐻𝑁) ∪ (𝑋𝐶𝑁))) |
| 4 | 3 | adantll 714 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋(ClWWalksNOn‘𝐺)𝑁) = ((𝑋𝐻𝑁) ∪ (𝑋𝐶𝑁))) |
| 5 | 4 | fveq2d 6910 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = (♯‘((𝑋𝐻𝑁) ∪ (𝑋𝐶𝑁)))) |
| 6 | 2 | numclwwlkovh0 30391 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐻𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋}) |
| 7 | 6 | adantll 714 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐻𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋}) |
| 8 | | eqid 2737 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 9 | 8 | fusgrvtxfi 29336 |
. . . . . 6
⊢ (𝐺 ∈ FinUSGraph →
(Vtx‘𝐺) ∈
Fin) |
| 10 | 9 | ad2antrr 726 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (Vtx‘𝐺) ∈
Fin) |
| 11 | 8 | clwwlknonfin 30113 |
. . . . 5
⊢
((Vtx‘𝐺)
∈ Fin → (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin) |
| 12 | | rabfi 9303 |
. . . . 5
⊢ ((𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin → {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋} ∈ Fin) |
| 13 | 10, 11, 12 | 3syl 18 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋} ∈ Fin) |
| 14 | 7, 13 | eqeltrd 2841 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐻𝑁) ∈ Fin) |
| 15 | 1 | 2clwwlk 30366 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) |
| 16 | 15 | adantll 714 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) |
| 17 | | rabfi 9303 |
. . . . 5
⊢ ((𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin → {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ Fin) |
| 18 | 10, 11, 17 | 3syl 18 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ Fin) |
| 19 | 16, 18 | eqeltrd 2841 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐶𝑁) ∈ Fin) |
| 20 | 7, 16 | ineq12d 4221 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑋𝐻𝑁) ∩ (𝑋𝐶𝑁)) = ({𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋} ∩ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})) |
| 21 | | inrab 4316 |
. . . . 5
⊢ ({𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋} ∩ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ ((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋)} |
| 22 | | exmid 895 |
. . . . . . . 8
⊢ ((𝑤‘(𝑁 − 2)) = 𝑋 ∨ ¬ (𝑤‘(𝑁 − 2)) = 𝑋) |
| 23 | | ianor 984 |
. . . . . . . . 9
⊢ (¬
((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ (¬ (𝑤‘(𝑁 − 2)) ≠ 𝑋 ∨ ¬ (𝑤‘(𝑁 − 2)) = 𝑋)) |
| 24 | | nne 2944 |
. . . . . . . . . 10
⊢ (¬
(𝑤‘(𝑁 − 2)) ≠ 𝑋 ↔ (𝑤‘(𝑁 − 2)) = 𝑋) |
| 25 | 24 | orbi1i 914 |
. . . . . . . . 9
⊢ ((¬
(𝑤‘(𝑁 − 2)) ≠ 𝑋 ∨ ¬ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((𝑤‘(𝑁 − 2)) = 𝑋 ∨ ¬ (𝑤‘(𝑁 − 2)) = 𝑋)) |
| 26 | 23, 25 | bitri 275 |
. . . . . . . 8
⊢ (¬
((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) ↔ ((𝑤‘(𝑁 − 2)) = 𝑋 ∨ ¬ (𝑤‘(𝑁 − 2)) = 𝑋)) |
| 27 | 22, 26 | mpbir 231 |
. . . . . . 7
⊢ ¬
((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) |
| 28 | 27 | rgenw 3065 |
. . . . . 6
⊢
∀𝑤 ∈
(𝑋(ClWWalksNOn‘𝐺)𝑁) ¬ ((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋) |
| 29 | | rabeq0 4388 |
. . . . . 6
⊢ ({𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ ((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋)} = ∅ ↔ ∀𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ¬ ((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋)) |
| 30 | 28, 29 | mpbir 231 |
. . . . 5
⊢ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ ((𝑤‘(𝑁 − 2)) ≠ 𝑋 ∧ (𝑤‘(𝑁 − 2)) = 𝑋)} = ∅ |
| 31 | 21, 30 | eqtri 2765 |
. . . 4
⊢ ({𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋} ∩ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) = ∅ |
| 32 | 20, 31 | eqtrdi 2793 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑋𝐻𝑁) ∩ (𝑋𝐶𝑁)) = ∅) |
| 33 | | hashun 14421 |
. . 3
⊢ (((𝑋𝐻𝑁) ∈ Fin ∧ (𝑋𝐶𝑁) ∈ Fin ∧ ((𝑋𝐻𝑁) ∩ (𝑋𝐶𝑁)) = ∅) → (♯‘((𝑋𝐻𝑁) ∪ (𝑋𝐶𝑁))) = ((♯‘(𝑋𝐻𝑁)) + (♯‘(𝑋𝐶𝑁)))) |
| 34 | 14, 19, 32, 33 | syl3anc 1373 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (♯‘((𝑋𝐻𝑁) ∪ (𝑋𝐶𝑁))) = ((♯‘(𝑋𝐻𝑁)) + (♯‘(𝑋𝐶𝑁)))) |
| 35 | 5, 34 | eqtrd 2777 |
1
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = ((♯‘(𝑋𝐻𝑁)) + (♯‘(𝑋𝐶𝑁)))) |