| Step | Hyp | Ref
| Expression |
| 1 | | frgr2wwlkeu.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | 1 | frgr2wwlkn0 30347 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(2 WWalksNOn 𝐺)𝐵) ≠ ∅) |
| 3 | 1 | elwwlks2ons3 29975 |
. . . . . 6
⊢ (𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 4 | 1 | elwwlks2ons3 29975 |
. . . . . 6
⊢ (𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 5 | 3, 4 | anbi12i 628 |
. . . . 5
⊢ ((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ↔ (∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
| 6 | 1 | frgr2wwlkeu 30346 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑥 ∈ 𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
| 7 | | s3eq2 14909 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 〈“𝐴𝑥𝐵”〉 = 〈“𝐴𝑦𝐵”〉) |
| 8 | 7 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 9 | 8 | reu4 3737 |
. . . . . . . . . . . 12
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (∃𝑥 ∈ 𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦))) |
| 10 | | s3eq2 14909 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑑 → 〈“𝐴𝑥𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
| 11 | 10 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑑 → (〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 12 | 11 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑑 → ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ↔ (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
| 13 | | equequ1 2024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑑 → (𝑥 = 𝑦 ↔ 𝑑 = 𝑦)) |
| 14 | 12, 13 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑑 → (((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦) ↔ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑦))) |
| 15 | | s3eq2 14909 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑐 → 〈“𝐴𝑦𝐵”〉 = 〈“𝐴𝑐𝐵”〉) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑐 → (〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 17 | 16 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑐 → ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ↔ (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
| 18 | | equequ2 2025 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑐 → (𝑑 = 𝑦 ↔ 𝑑 = 𝑐)) |
| 19 | 17, 18 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑐 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑦) ↔ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐))) |
| 20 | 14, 19 | rspc2va 3634 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦)) → ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐)) |
| 21 | | pm3.35 803 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐)) → 𝑑 = 𝑐) |
| 22 | | s3eq2 14909 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 = 𝑑 → 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
| 23 | 22 | equcoms 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑑 = 𝑐 → 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
| 25 | | eqeq12 2754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → (𝑡 = 𝑤 ↔ 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉)) |
| 26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → (𝑡 = 𝑤 ↔ 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉)) |
| 27 | 24, 26 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → 𝑡 = 𝑤) |
| 28 | 27 | equcomd 2018 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → 𝑤 = 𝑡) |
| 29 | 28 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = 𝑐 → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → 𝑤 = 𝑡)) |
| 30 | 21, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → 𝑤 = 𝑡)) |
| 31 | 30 | ex 412 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → 𝑤 = 𝑡))) |
| 32 | 31 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))) |
| 33 | 32 | exp4b 430 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝑡 = 〈“𝐴𝑐𝐵”〉 → (𝑤 = 〈“𝐴𝑑𝐵”〉 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))))) |
| 34 | 33 | com13 88 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 〈“𝐴𝑐𝐵”〉 → (〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝑤 = 〈“𝐴𝑑𝐵”〉 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))))) |
| 35 | 34 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝑤 = 〈“𝐴𝑑𝐵”〉 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡)))) |
| 36 | 35 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈“𝐴𝑑𝐵”〉 → (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡)))) |
| 37 | 36 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))) |
| 38 | 37 | com13 88 |
. . . . . . . . . . . . . 14
⊢
(((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
| 39 | 20, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
| 40 | 39 | expcom 413 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦) → ((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)))) |
| 41 | 9, 40 | simplbiim 504 |
. . . . . . . . . . 11
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)))) |
| 42 | 41 | impl 455 |
. . . . . . . . . 10
⊢
(((∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑑 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
| 43 | 42 | rexlimdva 3155 |
. . . . . . . . 9
⊢
((∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑑 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
| 44 | 43 | com23 86 |
. . . . . . . 8
⊢
((∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑑 ∈ 𝑉) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
| 45 | 44 | rexlimdva 3155 |
. . . . . . 7
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
| 46 | 45 | impd 410 |
. . . . . 6
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) → 𝑤 = 𝑡)) |
| 47 | 6, 46 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) → 𝑤 = 𝑡)) |
| 48 | 5, 47 | biimtrid 242 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)) |
| 49 | 48 | alrimivv 1928 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∀𝑤∀𝑡((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)) |
| 50 | | eqeuel 4365 |
. . 3
⊢ (((𝐴(2 WWalksNOn 𝐺)𝐵) ≠ ∅ ∧ ∀𝑤∀𝑡((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)) → ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
| 51 | 2, 49, 50 | syl2anc 584 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
| 52 | | ovex 7464 |
. . 3
⊢ (𝐴(2 WWalksNOn 𝐺)𝐵) ∈ V |
| 53 | | euhash1 14459 |
. . 3
⊢ ((𝐴(2 WWalksNOn 𝐺)𝐵) ∈ V → ((♯‘(𝐴(2 WWalksNOn 𝐺)𝐵)) = 1 ↔ ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 54 | 52, 53 | mp1i 13 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((♯‘(𝐴(2 WWalksNOn 𝐺)𝐵)) = 1 ↔ ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 55 | 51, 54 | mpbird 257 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (♯‘(𝐴(2 WWalksNOn 𝐺)𝐵)) = 1) |