Step | Hyp | Ref
| Expression |
1 | | df-ewlks 40799 |
. . . 4
⊢ EdgWalks
= (𝑔 ∈ V, 𝑠 ∈
ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))}) |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ EdgWalks = (𝑔 ∈
V, 𝑠 ∈
ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})) |
3 | | fvex 6113 |
. . . . . . 7
⊢
(iEdg‘𝑔)
∈ V |
4 | 3 | a1i 11 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (iEdg‘𝑔) ∈ V) |
5 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → 𝑖 = (iEdg‘𝑔)) |
6 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺)) |
7 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (iEdg‘𝑔) = (iEdg‘𝐺)) |
8 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (iEdg‘𝑔) = (iEdg‘𝐺)) |
9 | 5, 8 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → 𝑖 = (iEdg‘𝐺)) |
10 | 9 | dmeqd 5248 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → dom 𝑖 = dom (iEdg‘𝐺)) |
11 | | wrdeq 13182 |
. . . . . . . . 9
⊢ (dom
𝑖 = dom (iEdg‘𝐺) → Word dom 𝑖 = Word dom (iEdg‘𝐺)) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → Word dom 𝑖 = Word dom (iEdg‘𝐺)) |
13 | 12 | eleq2d 2673 |
. . . . . . 7
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑓 ∈ Word dom 𝑖 ↔ 𝑓 ∈ Word dom (iEdg‘𝐺))) |
14 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
15 | 14 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → 𝑠 = 𝑆) |
16 | 9 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑖‘(𝑓‘(𝑘 − 1))) = ((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1)))) |
17 | 9 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑖‘(𝑓‘𝑘)) = ((iEdg‘𝐺)‘(𝑓‘𝑘))) |
18 | 16, 17 | ineq12d 3777 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → ((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))) = (((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) |
19 | 18 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))) = (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))) |
20 | 15, 19 | breq12d 4596 |
. . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))) ↔ 𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))) |
21 | 20 | ralbidv 2969 |
. . . . . . 7
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))) ↔ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))) |
22 | 13, 21 | anbi12d 743 |
. . . . . 6
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → ((𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))) ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))))) |
23 | 4, 22 | sbcied 3439 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → ([(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))) ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))))) |
24 | 23 | abbidv 2728 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))} = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))}) |
25 | 24 | adantl 481 |
. . 3
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))} = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))}) |
26 | | elex 3185 |
. . . 4
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) |
27 | 26 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ 𝐺 ∈
V) |
28 | | simpr 476 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ 𝑆 ∈
ℕ0*) |
29 | | df-rab 2905 |
. . . 4
⊢ {𝑓 ∈ Word dom
(iEdg‘𝐺) ∣
∀𝑘 ∈
(1..^(#‘𝑓))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))} = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))} |
30 | | fvex 6113 |
. . . . . . . 8
⊢
(iEdg‘𝐺)
∈ V |
31 | 30 | dmex 6991 |
. . . . . . 7
⊢ dom
(iEdg‘𝐺) ∈
V |
32 | 31 | wrdexi 13172 |
. . . . . 6
⊢ Word dom
(iEdg‘𝐺) ∈
V |
33 | 32 | rabex 4740 |
. . . . 5
⊢ {𝑓 ∈ Word dom
(iEdg‘𝐺) ∣
∀𝑘 ∈
(1..^(#‘𝑓))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))} ∈ V |
34 | 33 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ {𝑓 ∈ Word dom
(iEdg‘𝐺) ∣
∀𝑘 ∈
(1..^(#‘𝑓))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))} ∈ V) |
35 | 29, 34 | syl5eqelr 2693 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ {𝑓 ∣ (𝑓 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(#‘𝑓))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))} ∈ V) |
36 | 2, 25, 27, 28, 35 | ovmpt2d 6686 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))}) |
37 | | ewlksfval.i |
. . . . . . . . 9
⊢ 𝐼 = (iEdg‘𝐺) |
38 | 37 | eqcomi 2619 |
. . . . . . . 8
⊢
(iEdg‘𝐺) =
𝐼 |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (iEdg‘𝐺) =
𝐼) |
40 | 39 | dmeqd 5248 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ dom (iEdg‘𝐺) =
dom 𝐼) |
41 | | wrdeq 13182 |
. . . . . 6
⊢ (dom
(iEdg‘𝐺) = dom 𝐼 → Word dom
(iEdg‘𝐺) = Word dom
𝐼) |
42 | 40, 41 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ Word dom (iEdg‘𝐺) = Word dom 𝐼) |
43 | 42 | eleq2d 2673 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝑓 ∈ Word dom
(iEdg‘𝐺) ↔ 𝑓 ∈ Word dom 𝐼)) |
44 | 39 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ ((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) = (𝐼‘(𝑓‘(𝑘 − 1)))) |
45 | 39 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ ((iEdg‘𝐺)‘(𝑓‘𝑘)) = (𝐼‘(𝑓‘𝑘))) |
46 | 44, 45 | ineq12d 3777 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))) = ((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))) |
47 | 46 | fveq2d 6107 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) = (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘))))) |
48 | 47 | breq2d 4595 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) ↔ 𝑆 ≤ (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))) |
49 | 48 | ralbidv 2969 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (∀𝑘 ∈
(1..^(#‘𝑓))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) ↔ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))) |
50 | 43, 49 | anbi12d 743 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ ((𝑓 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(#‘𝑓))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))) ↔ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘))))))) |
51 | 50 | abbidv 2728 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ {𝑓 ∣ (𝑓 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(#‘𝑓))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))} = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))}) |
52 | 36, 51 | eqtrd 2644 |
1
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))}) |