Step | Hyp | Ref
| Expression |
1 | | simpr1 1060 |
. . . . . . . . . . 11
⊢
(((#‘𝑓) = 2
∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵)) → 𝑉 USGrph 𝐸) |
2 | | simpl 472 |
. . . . . . . . . . 11
⊢
(((#‘𝑓) = 2
∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵)) → (#‘𝑓) = 2) |
3 | | simpr3 1062 |
. . . . . . . . . . 11
⊢
(((#‘𝑓) = 2
∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ≠ 𝐵) |
4 | | usgra2wlkspth 26149 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝑓) = 2 ∧ 𝐴 ≠ 𝐵) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ↔ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝)) |
5 | 1, 2, 3, 4 | syl3anc 1318 |
. . . . . . . . . 10
⊢
(((#‘𝑓) = 2
∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵)) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ↔ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝)) |
6 | 5 | bicomd 212 |
. . . . . . . . 9
⊢
(((#‘𝑓) = 2
∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵)) → (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ↔ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝)) |
7 | 6 | ex 449 |
. . . . . . . 8
⊢
((#‘𝑓) = 2
→ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ↔ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝))) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢
(((#‘𝑓) = 2
∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)) → ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ↔ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝))) |
9 | 8 | com12 32 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (((#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)) → (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ↔ 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝))) |
10 | 9 | pm5.32rd 670 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ ((#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))) ↔ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ ((#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))))) |
11 | | 3anass 1035 |
. . . . 5
⊢ ((𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)) ↔ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ ((#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)))) |
12 | | 3anass 1035 |
. . . . 5
⊢ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)) ↔ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ ((#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)))) |
13 | 10, 11, 12 | 3bitr4g 302 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)) ↔ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)))) |
14 | 13 | 2exbidv 1839 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)) ↔ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵)))) |
15 | 14 | rabbidv 3164 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) |
16 | | usgrav 25867 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
17 | | 2spthonot 26393 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) |
18 | 16, 17 | sylan 487 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) |
19 | 18 | 3adant3 1074 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) |
20 | | 2wlkonot 26392 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) |
21 | 16, 20 | sylan 487 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) |
22 | 21 | 3adant3 1074 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) |
23 | 15, 19, 22 | 3eqtr4d 2654 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐵) = (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) |