| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | wlkson.v | . . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) | 
| 2 | 1 | fvexi 6920 | . . . . 5
⊢ 𝑉 ∈ V | 
| 3 |  | df-wlkson 29618 | . . . . . 6
⊢ WalksOn =
(𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)})) | 
| 4 | 1 | wlkson 29674 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(WalksOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(♯‘𝑓)) = 𝐵)}) | 
| 5 | 4 | 3adant1 1131 | . . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(WalksOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(♯‘𝑓)) = 𝐵)}) | 
| 6 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) | 
| 7 | 6, 1 | eqtr4di 2795 | . . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) | 
| 8 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (Walks‘𝑔) = (Walks‘𝐺)) | 
| 9 | 8 | breqd 5154 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑓(Walks‘𝑔)𝑝 ↔ 𝑓(Walks‘𝐺)𝑝)) | 
| 10 | 9 | 3anbi1d 1442 | . . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏) ↔ (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏))) | 
| 11 | 3, 5, 7, 7, 10 | bropfvvvv 8117 | . . . . 5
⊢ ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → (𝐺 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) | 
| 12 | 2, 2, 11 | mp2an 692 | . . . 4
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → (𝐺 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | 
| 13 |  | 3anass 1095 | . . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ↔ (𝐺 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) | 
| 14 | 13 | anbi1i 624 | . . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ↔ ((𝐺 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | 
| 15 |  | df-3an 1089 | . . . . 5
⊢ ((𝐺 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ↔ ((𝐺 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | 
| 16 | 14, 15 | bitr4i 278 | . . . 4
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ↔ (𝐺 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | 
| 17 | 12, 16 | sylibr 234 | . . 3
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | 
| 18 | 1 | iswlkon 29675 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | 
| 19 | 18 | 3adantl1 1167 | . . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | 
| 20 | 19 | biimpd 229 | . . . 4
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | 
| 21 | 20 | imdistani 568 | . . 3
⊢ ((((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃) → (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | 
| 22 | 17, 21 | mpancom 688 | . 2
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | 
| 23 |  | df-3an 1089 | . 2
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) ↔ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | 
| 24 | 22, 23 | sylibr 234 | 1
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) |