Step | Hyp | Ref
| Expression |
1 | | frg2wotn0 26583 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ≠ ∅) |
2 | | frisusgra 26519 |
. . . . . . . . . . . . 13
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
3 | | usgrav 25867 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
5 | 4 | anim1i 590 |
. . . . . . . . . . 11
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
6 | 5 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
7 | | el2wlkonot 26396 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))))) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))))) |
9 | | el2wlkonot 26396 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∃𝑐 ∈ 𝑉 (𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))))) |
10 | 6, 9 | syl 17 |
. . . . . . . . 9
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∃𝑐 ∈ 𝑉 (𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))))) |
11 | 8, 10 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) ↔ (∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2))))))) |
12 | | frg2woteu 26582 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑥 ∈ 𝑉 〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) |
13 | | oteq2 4350 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑦 → 〈𝐴, 𝑥, 𝐵〉 = 〈𝐴, 𝑦, 𝐵〉) |
14 | 13 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑦 → (〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
15 | 14 | reu4 3367 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃!𝑥 ∈
𝑉 〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ (∃𝑥 ∈ 𝑉 〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑥 = 𝑦))) |
16 | | oteq2 4350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = 𝑐 → 〈𝐴, 𝑥, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉) |
17 | 16 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = 𝑐 → (〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
18 | 17 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = 𝑐 → ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) ↔ (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)))) |
19 | | ancom 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) ↔ (〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
20 | 18, 19 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑐 → ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) ↔ (〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)))) |
21 | | equequ1 1939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = 𝑐 → (𝑥 = 𝑦 ↔ 𝑐 = 𝑦)) |
22 | | equcom 1932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = 𝑦 ↔ 𝑦 = 𝑐) |
23 | 21, 22 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑐 → (𝑥 = 𝑦 ↔ 𝑦 = 𝑐)) |
24 | 20, 23 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 𝑐 → (((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑥 = 𝑦) ↔ ((〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑦 = 𝑐))) |
25 | | oteq2 4350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = 𝑑 → 〈𝐴, 𝑦, 𝐵〉 = 〈𝐴, 𝑑, 𝐵〉) |
26 | 25 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = 𝑑 → (〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ 〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
27 | 26 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = 𝑑 → ((〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) ↔ (〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)))) |
28 | | equequ1 1939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = 𝑑 → (𝑦 = 𝑐 ↔ 𝑑 = 𝑐)) |
29 | 27, 28 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = 𝑑 → (((〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑦 = 𝑐) ↔ ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑑 = 𝑐))) |
30 | 24, 29 | rspc2va 3294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑥 = 𝑦)) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑑 = 𝑐)) |
31 | | oteq2 4350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑑 = 𝑐 → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉) |
32 | 30, 31 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑥 = 𝑦)) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉)) |
33 | 32 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑥 = 𝑦) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉))) |
34 | 33 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑉 ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑥 = 𝑦) → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉))) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∃𝑥 ∈
𝑉 〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑦, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑥 = 𝑦)) → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉))) |
36 | 15, 35 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃!𝑥 ∈
𝑉 〈𝐴, 𝑥, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉))) |
37 | 12, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉))) |
38 | 37 | impl 648 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉)) |
39 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 〈𝐴, 𝑑, 𝐵〉 → (𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ 〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
40 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 〈𝐴, 𝑐, 𝐵〉 → (𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
41 | 39, 40 | bi2anan9 913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ 𝑡 = 〈𝐴, 𝑐, 𝐵〉) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) ↔ (〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)))) |
42 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ 𝑡 = 〈𝐴, 𝑐, 𝐵〉) → (𝑤 = 𝑡 ↔ 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉)) |
43 | 41, 42 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ 𝑡 = 〈𝐴, 𝑐, 𝐵〉) → (((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡) ↔ ((〈𝐴, 𝑑, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 〈𝐴, 𝑑, 𝐵〉 = 〈𝐴, 𝑐, 𝐵〉))) |
44 | 38, 43 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ 𝑡 = 〈𝐴, 𝑐, 𝐵〉) → ((((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡))) |
45 | 44 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 〈𝐴, 𝑑, 𝐵〉 → (𝑡 = 〈𝐴, 𝑐, 𝐵〉 → ((((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
46 | 45 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈𝐴, 𝑑, 𝐵〉 → ((((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → (𝑡 = 〈𝐴, 𝑐, 𝐵〉 → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → (𝑡 = 〈𝐴, 𝑐, 𝐵〉 → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
48 | 47 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (𝑡 = 〈𝐴, 𝑐, 𝐵〉 → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
49 | 48 | rexlimdva 3013 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) → (∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (𝑡 = 〈𝐴, 𝑐, 𝐵〉 → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
50 | 49 | com23 84 |
. . . . . . . . . . . . 13
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) → (𝑡 = 〈𝐴, 𝑐, 𝐵〉 → (∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
51 | 50 | adantrd 483 |
. . . . . . . . . . . 12
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑐 ∈ 𝑉) → ((𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
52 | 51 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
53 | 52 | com13 86 |
. . . . . . . . . 10
⊢
(∃𝑑 ∈
𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)))) |
54 | 53 | imp 444 |
. . . . . . . . 9
⊢
((∃𝑑 ∈
𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2))))) → ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡))) |
55 | 54 | com12 32 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((∃𝑑 ∈ 𝑉 (𝑤 = 〈𝐴, 𝑑, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2))))) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡))) |
56 | 11, 55 | sylbid 229 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡))) |
57 | 56 | pm2.43d 51 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)) |
58 | 57 | alrimivv 1843 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∀𝑤∀𝑡((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)) |
59 | | eleq1 2676 |
. . . . . 6
⊢ (𝑤 = 𝑡 → (𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
60 | 59 | mo4 2505 |
. . . . 5
⊢
(∃*𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∀𝑤∀𝑡((𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑡 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) → 𝑤 = 𝑡)) |
61 | 58, 60 | sylibr 223 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃*𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) |
62 | | n0moeu 3893 |
. . . 4
⊢ ((𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ≠ ∅ → (∃*𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∃!𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
63 | 61, 62 | syl5ib 233 |
. . 3
⊢ ((𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ≠ ∅ → ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
64 | 1, 63 | mpcom 37 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) |
65 | | ovex 6577 |
. . 3
⊢ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∈ V |
66 | | euhash1 13069 |
. . 3
⊢ ((𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∈ V → ((#‘(𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) = 1 ↔ ∃!𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
67 | 65, 66 | mp1i 13 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((#‘(𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) = 1 ↔ ∃!𝑤 𝑤 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
68 | 64, 67 | mpbird 246 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (#‘(𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) = 1) |