| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) = (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
| 2 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑠 = 𝑤 → (♯‘(1st
‘𝑠)) =
(♯‘(1st ‘𝑤))) |
| 3 | 2 | breq2d 5155 |
. . . . . . 7
⊢ (𝑠 = 𝑤 → (1 ≤
(♯‘(1st ‘𝑠)) ↔ 1 ≤
(♯‘(1st ‘𝑤)))) |
| 4 | 3 | cbvrabv 3447 |
. . . . . 6
⊢ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} = {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} |
| 5 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → (2nd ‘𝑑) = (2nd ‘𝑐)) |
| 6 | | 2fveq3 6911 |
. . . . . . . . 9
⊢ (𝑑 = 𝑐 → (♯‘(2nd
‘𝑑)) =
(♯‘(2nd ‘𝑐))) |
| 7 | 6 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → ((♯‘(2nd
‘𝑑)) − 1) =
((♯‘(2nd ‘𝑐)) − 1)) |
| 8 | 5, 7 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑑 = 𝑐 → ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1)) = ((2nd
‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
| 9 | 8 | cbvmptv 5255 |
. . . . . 6
⊢ (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1))) = (𝑐 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
| 10 | 4, 9 | clwlkclwwlkf1o 30030 |
. . . . 5
⊢ (𝐺 ∈ USPGraph → (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1))):{𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))}–1-1-onto→(ClWWalks‘𝐺)) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1))):{𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))}–1-1-onto→(ClWWalks‘𝐺)) |
| 12 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑠 → (♯‘(1st
‘𝑤)) =
(♯‘(1st ‘𝑠))) |
| 13 | 12 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑤 = 𝑠 → (1 ≤
(♯‘(1st ‘𝑤)) ↔ 1 ≤
(♯‘(1st ‘𝑠)))) |
| 14 | 13 | cbvrabv 3447 |
. . . . . . . 8
⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} = {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} |
| 15 | 14 | mpteq1i 5238 |
. . . . . . 7
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) = (𝑐 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
| 16 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑐 = 𝑑 → (2nd ‘𝑐) = (2nd ‘𝑑)) |
| 17 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑑 → (♯‘(2nd
‘𝑐)) =
(♯‘(2nd ‘𝑑))) |
| 18 | 17 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑐 = 𝑑 → ((♯‘(2nd
‘𝑐)) − 1) =
((♯‘(2nd ‘𝑑)) − 1)) |
| 19 | 16, 18 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑐 = 𝑑 → ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1)) = ((2nd
‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1))) |
| 20 | 19 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑐 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) = (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1))) |
| 21 | 15, 20 | eqtri 2765 |
. . . . . 6
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) = (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1))) |
| 22 | 21 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) = (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1)))) |
| 23 | 4 | eqcomi 2746 |
. . . . . 6
⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} = {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} |
| 24 | 23 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} = {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))}) |
| 25 | | eqidd 2738 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) →
(ClWWalks‘𝐺) =
(ClWWalks‘𝐺)) |
| 26 | 22, 24, 25 | f1oeq123d 6842 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))):{𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))}–1-1-onto→(ClWWalks‘𝐺) ↔ (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) prefix
((♯‘(2nd ‘𝑑)) − 1))):{𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑠))}–1-1-onto→(ClWWalks‘𝐺))) |
| 27 | 11, 26 | mpbird 257 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))):{𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))}–1-1-onto→(ClWWalks‘𝐺)) |
| 28 | | fveq2 6906 |
. . . . . 6
⊢ (𝑠 = ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1)) → (♯‘𝑠) =
(♯‘((2nd ‘𝑐) prefix ((♯‘(2nd
‘𝑐)) −
1)))) |
| 29 | 28 | 3ad2ant3 1136 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) prefix ((♯‘(2nd
‘𝑐)) − 1)))
→ (♯‘𝑠) =
(♯‘((2nd ‘𝑐) prefix ((♯‘(2nd
‘𝑐)) −
1)))) |
| 30 | | 2fveq3 6911 |
. . . . . . . . 9
⊢ (𝑤 = 𝑐 → (♯‘(1st
‘𝑤)) =
(♯‘(1st ‘𝑐))) |
| 31 | 30 | breq2d 5155 |
. . . . . . . 8
⊢ (𝑤 = 𝑐 → (1 ≤
(♯‘(1st ‘𝑤)) ↔ 1 ≤
(♯‘(1st ‘𝑐)))) |
| 32 | 31 | elrab 3692 |
. . . . . . 7
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤
(♯‘(1st ‘𝑐)))) |
| 33 | | clwlknf1oclwwlknlem1 30100 |
. . . . . . 7
⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤
(♯‘(1st ‘𝑐))) → (♯‘((2nd
‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) =
(♯‘(1st ‘𝑐))) |
| 34 | 32, 33 | sylbi 217 |
. . . . . 6
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} → (♯‘((2nd
‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) =
(♯‘(1st ‘𝑐))) |
| 35 | 34 | 3ad2ant2 1135 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) prefix ((♯‘(2nd
‘𝑐)) − 1)))
→ (♯‘((2nd ‘𝑐) prefix ((♯‘(2nd
‘𝑐)) − 1))) =
(♯‘(1st ‘𝑐))) |
| 36 | 29, 35 | eqtrd 2777 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) prefix ((♯‘(2nd
‘𝑐)) − 1)))
→ (♯‘𝑠) =
(♯‘(1st ‘𝑐))) |
| 37 | 36 | eqeq1d 2739 |
. . 3
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) prefix ((♯‘(2nd
‘𝑐)) − 1)))
→ ((♯‘𝑠) =
𝑁 ↔
(♯‘(1st ‘𝑐)) = 𝑁)) |
| 38 | 1, 27, 37 | f1oresrab 7147 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁}):{𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁}–1-1-onto→{𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁}) |
| 39 | | clwlknf1oclwwlkn.a |
. . . . 5
⊢ 𝐴 = (1st ‘𝑐) |
| 40 | | clwlknf1oclwwlkn.b |
. . . . 5
⊢ 𝐵 = (2nd ‘𝑐) |
| 41 | | clwlknf1oclwwlkn.c |
. . . . 5
⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = 𝑁} |
| 42 | | clwlknf1oclwwlkn.f |
. . . . 5
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 prefix (♯‘𝐴))) |
| 43 | 39, 40, 41, 42 | clwlknf1oclwwlknlem3 30102 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ (𝐵 prefix (♯‘𝐴))) ↾ 𝐶)) |
| 44 | 40 | a1i 11 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))}) → 𝐵 = (2nd ‘𝑐)) |
| 45 | | clwlkwlk 29795 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (ClWalks‘𝐺) → 𝑐 ∈ (Walks‘𝐺)) |
| 46 | | wlkcpr 29647 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ (Walks‘𝐺) ↔ (1st
‘𝑐)(Walks‘𝐺)(2nd ‘𝑐)) |
| 47 | 39 | fveq2i 6909 |
. . . . . . . . . . . . 13
⊢
(♯‘𝐴) =
(♯‘(1st ‘𝑐)) |
| 48 | | wlklenvm1 29640 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (♯‘(1st
‘𝑐)) =
((♯‘(2nd ‘𝑐)) − 1)) |
| 49 | 47, 48 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (♯‘𝐴) = ((♯‘(2nd
‘𝑐)) −
1)) |
| 50 | 46, 49 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (Walks‘𝐺) → (♯‘𝐴) =
((♯‘(2nd ‘𝑐)) − 1)) |
| 51 | 45, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (ClWalks‘𝐺) → (♯‘𝐴) =
((♯‘(2nd ‘𝑐)) − 1)) |
| 52 | 51 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤
(♯‘(1st ‘𝑐))) → (♯‘𝐴) = ((♯‘(2nd
‘𝑐)) −
1)) |
| 53 | 32, 52 | sylbi 217 |
. . . . . . . 8
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} → (♯‘𝐴) = ((♯‘(2nd
‘𝑐)) −
1)) |
| 54 | 53 | adantl 481 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))}) → (♯‘𝐴) = ((♯‘(2nd
‘𝑐)) −
1)) |
| 55 | 44, 54 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))}) → (𝐵 prefix (♯‘𝐴)) = ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
| 56 | 55 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ (𝐵 prefix (♯‘𝐴))) = (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1)))) |
| 57 | 30 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑤 = 𝑐 → ((♯‘(1st
‘𝑤)) = 𝑁 ↔
(♯‘(1st ‘𝑐)) = 𝑁)) |
| 58 | 57 | cbvrabv 3447 |
. . . . . . 7
⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣
(♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st
‘𝑐)) = 𝑁} |
| 59 | | nnge1 12294 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
| 60 | | breq2 5147 |
. . . . . . . . . . . 12
⊢
((♯‘(1st ‘𝑐)) = 𝑁 → (1 ≤
(♯‘(1st ‘𝑐)) ↔ 1 ≤ 𝑁)) |
| 61 | 59, 60 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
((♯‘(1st ‘𝑐)) = 𝑁 → 1 ≤
(♯‘(1st ‘𝑐)))) |
| 62 | 61 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) →
((♯‘(1st ‘𝑐)) = 𝑁 → 1 ≤
(♯‘(1st ‘𝑐)))) |
| 63 | 62 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) →
((♯‘(1st ‘𝑐)) = 𝑁 → 1 ≤
(♯‘(1st ‘𝑐)))) |
| 64 | 63 | pm4.71rd 562 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) →
((♯‘(1st ‘𝑐)) = 𝑁 ↔ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁))) |
| 65 | 64 | rabbidva 3443 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑐 ∈ (ClWalks‘𝐺) ∣
(♯‘(1st ‘𝑐)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁)}) |
| 66 | 58, 65 | eqtrid 2789 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣
(♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁)}) |
| 67 | 32 | anbi1i 624 |
. . . . . . . 8
⊢ ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∧ (♯‘(1st
‘𝑐)) = 𝑁) ↔ ((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤
(♯‘(1st ‘𝑐))) ∧ (♯‘(1st
‘𝑐)) = 𝑁)) |
| 68 | | anass 468 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤
(♯‘(1st ‘𝑐))) ∧ (♯‘(1st
‘𝑐)) = 𝑁) ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁))) |
| 69 | 67, 68 | bitri 275 |
. . . . . . 7
⊢ ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∧ (♯‘(1st
‘𝑐)) = 𝑁) ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁))) |
| 70 | 69 | rabbia2 3439 |
. . . . . 6
⊢ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁)} |
| 71 | 66, 41, 70 | 3eqtr4g 2802 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐶 = {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁}) |
| 72 | 56, 71 | reseq12d 5998 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ (𝐵 prefix (♯‘𝐴))) ↾ 𝐶) = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁})) |
| 73 | 43, 72 | eqtrd 2777 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁})) |
| 74 | | clwlknf1oclwwlknlem2 30101 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {𝑤 ∈ (ClWalks‘𝐺) ∣
(♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁)}) |
| 75 | 74 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣
(♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤
(♯‘(1st ‘𝑐)) ∧ (♯‘(1st
‘𝑐)) = 𝑁)}) |
| 76 | 75, 41, 70 | 3eqtr4g 2802 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐶 = {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁}) |
| 77 | | clwwlkn 30045 |
. . . 4
⊢ (𝑁 ClWWalksN 𝐺) = {𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁} |
| 78 | 77 | a1i 11 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑁 ClWWalksN 𝐺) = {𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁}) |
| 79 | 73, 76, 78 | f1oeq123d 6842 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝐹:𝐶–1-1-onto→(𝑁 ClWWalksN 𝐺) ↔ ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁}):{𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} ∣ (♯‘(1st
‘𝑐)) = 𝑁}–1-1-onto→{𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁})) |
| 80 | 38, 79 | mpbird 257 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹:𝐶–1-1-onto→(𝑁 ClWWalksN 𝐺)) |