| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ewlks 29617 | . . . 4
⊢  EdgWalks
= (𝑔 ∈ V, 𝑠 ∈
ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))}) | 
| 2 | 1 | a1i 11 | . . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ EdgWalks = (𝑔 ∈
V, 𝑠 ∈
ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})) | 
| 3 |  | fvexd 6920 | . . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (iEdg‘𝑔) ∈ V) | 
| 4 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → 𝑖 = (iEdg‘𝑔)) | 
| 5 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺)) | 
| 6 | 5 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (iEdg‘𝑔) = (iEdg‘𝐺)) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (iEdg‘𝑔) = (iEdg‘𝐺)) | 
| 8 | 4, 7 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → 𝑖 = (iEdg‘𝐺)) | 
| 9 | 8 | dmeqd 5915 | . . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → dom 𝑖 = dom (iEdg‘𝐺)) | 
| 10 |  | wrdeq 14575 | . . . . . . . . 9
⊢ (dom
𝑖 = dom (iEdg‘𝐺) → Word dom 𝑖 = Word dom (iEdg‘𝐺)) | 
| 11 | 9, 10 | syl 17 | . . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → Word dom 𝑖 = Word dom (iEdg‘𝐺)) | 
| 12 | 11 | eleq2d 2826 | . . . . . . 7
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑓 ∈ Word dom 𝑖 ↔ 𝑓 ∈ Word dom (iEdg‘𝐺))) | 
| 13 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) | 
| 14 | 13 | adantr 480 | . . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → 𝑠 = 𝑆) | 
| 15 | 8 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑖‘(𝑓‘(𝑘 − 1))) = ((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1)))) | 
| 16 | 8 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑖‘(𝑓‘𝑘)) = ((iEdg‘𝐺)‘(𝑓‘𝑘))) | 
| 17 | 15, 16 | ineq12d 4220 | . . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → ((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))) = (((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) | 
| 18 | 17 | fveq2d 6909 | . . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))) = (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))) | 
| 19 | 14, 18 | breq12d 5155 | . . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))) ↔ 𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))) | 
| 20 | 19 | ralbidv 3177 | . . . . . . 7
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → (∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))) ↔ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))) | 
| 21 | 12, 20 | anbi12d 632 | . . . . . 6
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) ∧ 𝑖 = (iEdg‘𝑔)) → ((𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))) ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))))) | 
| 22 | 3, 21 | sbcied 3831 | . . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → ([(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))) ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))))) | 
| 23 | 22 | abbidv 2807 | . . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))} = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))}) | 
| 24 | 23 | adantl 481 | . . 3
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))} = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))}) | 
| 25 |  | elex 3500 | . . . 4
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) | 
| 26 | 25 | adantr 480 | . . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ 𝐺 ∈
V) | 
| 27 |  | simpr 484 | . . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ 𝑆 ∈
ℕ0*) | 
| 28 |  | df-rab 3436 | . . . 4
⊢ {𝑓 ∈ Word dom
(iEdg‘𝐺) ∣
∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))} = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))} | 
| 29 |  | fvex 6918 | . . . . . . . 8
⊢
(iEdg‘𝐺)
∈ V | 
| 30 | 29 | dmex 7932 | . . . . . . 7
⊢ dom
(iEdg‘𝐺) ∈
V | 
| 31 | 30 | wrdexi 14565 | . . . . . 6
⊢ Word dom
(iEdg‘𝐺) ∈
V | 
| 32 | 31 | rabex 5338 | . . . . 5
⊢ {𝑓 ∈ Word dom
(iEdg‘𝐺) ∣
∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))} ∈ V | 
| 33 | 32 | a1i 11 | . . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ {𝑓 ∈ Word dom
(iEdg‘𝐺) ∣
∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))} ∈ V) | 
| 34 | 28, 33 | eqeltrrid 2845 | . . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ {𝑓 ∣ (𝑓 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))} ∈ V) | 
| 35 | 2, 24, 26, 27, 34 | ovmpod 7586 | . 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))}) | 
| 36 |  | ewlksfval.i | . . . . . . . . 9
⊢ 𝐼 = (iEdg‘𝐺) | 
| 37 | 36 | eqcomi 2745 | . . . . . . . 8
⊢
(iEdg‘𝐺) =
𝐼 | 
| 38 | 37 | a1i 11 | . . . . . . 7
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (iEdg‘𝐺) =
𝐼) | 
| 39 | 38 | dmeqd 5915 | . . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ dom (iEdg‘𝐺) =
dom 𝐼) | 
| 40 |  | wrdeq 14575 | . . . . . 6
⊢ (dom
(iEdg‘𝐺) = dom 𝐼 → Word dom
(iEdg‘𝐺) = Word dom
𝐼) | 
| 41 | 39, 40 | syl 17 | . . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ Word dom (iEdg‘𝐺) = Word dom 𝐼) | 
| 42 | 41 | eleq2d 2826 | . . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝑓 ∈ Word dom
(iEdg‘𝐺) ↔ 𝑓 ∈ Word dom 𝐼)) | 
| 43 | 38 | fveq1d 6907 | . . . . . . . 8
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ ((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) = (𝐼‘(𝑓‘(𝑘 − 1)))) | 
| 44 | 38 | fveq1d 6907 | . . . . . . . 8
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ ((iEdg‘𝐺)‘(𝑓‘𝑘)) = (𝐼‘(𝑓‘𝑘))) | 
| 45 | 43, 44 | ineq12d 4220 | . . . . . . 7
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))) = ((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))) | 
| 46 | 45 | fveq2d 6909 | . . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) = (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘))))) | 
| 47 | 46 | breq2d 5154 | . . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝑆 ≤
(♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) ↔ 𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))) | 
| 48 | 47 | ralbidv 3177 | . . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))) ↔ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))) | 
| 49 | 42, 48 | anbi12d 632 | . . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ ((𝑓 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘))))) ↔ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘))))))) | 
| 50 | 49 | abbidv 2807 | . 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ {𝑓 ∣ (𝑓 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(♯‘𝑓))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝑓‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝑓‘𝑘)))))} = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))}) | 
| 51 | 35, 50 | eqtrd 2776 | 1
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*)
→ (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))}) |