Step | Hyp | Ref
| Expression |
1 | | frgr2wwlkeu.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | frgr2wwlkn0 27192 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(2 WWalksNOn 𝐺)𝐵) ≠ ∅) |
3 | 1 | elwwlks2ons3 26848 |
. . . . . . . 8
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
4 | 3 | 3expb 1266 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
5 | 4 | 3adant3 1081 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
6 | 1 | elwwlks2ons3 26848 |
. . . . . . . 8
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
7 | 6 | 3expb 1266 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
8 | 7 | 3adant3 1081 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
9 | 5, 8 | anbi12d 747 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ↔ (∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))))) |
10 | 1 | frgr2wwlkeu 27191 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑥 ∈ 𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
11 | | s3eq2 13615 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 〈“𝐴𝑥𝐵”〉 = 〈“𝐴𝑦𝐵”〉) |
12 | 11 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
13 | 12 | reu4 3400 |
. . . . . . . . . . . 12
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (∃𝑥 ∈ 𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦))) |
14 | | s3eq2 13615 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑑 → 〈“𝐴𝑥𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
15 | 14 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑑 → (〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
16 | 15 | anbi1d 741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑑 → ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ↔ (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
17 | | equequ1 1952 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑑 → (𝑥 = 𝑦 ↔ 𝑑 = 𝑦)) |
18 | 16, 17 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑑 → (((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦) ↔ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑦))) |
19 | | s3eq2 13615 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑐 → 〈“𝐴𝑦𝐵”〉 = 〈“𝐴𝑐𝐵”〉) |
20 | 19 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑐 → (〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
21 | 20 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑐 → ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ↔ (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)))) |
22 | | equequ2 1953 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑐 → (𝑑 = 𝑦 ↔ 𝑑 = 𝑐)) |
23 | 21, 22 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑐 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑦) ↔ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐))) |
24 | 18, 23 | rspc2va 3323 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦)) → ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐)) |
25 | | pm3.35 611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐)) → 𝑑 = 𝑐) |
26 | | s3eq2 13615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 = 𝑑 → 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
27 | 26 | equcoms 1947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑑 = 𝑐 → 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉) |
29 | | eqeq12 2635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → (𝑡 = 𝑤 ↔ 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉)) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → (𝑡 = 𝑤 ↔ 〈“𝐴𝑐𝐵”〉 = 〈“𝐴𝑑𝐵”〉)) |
31 | 28, 30 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → 𝑡 = 𝑤) |
32 | 31 | equcomd 1946 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉)) → 𝑤 = 𝑡) |
33 | 32 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = 𝑐 → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → 𝑤 = 𝑡)) |
34 | 25, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → 𝑤 = 𝑡)) |
35 | 34 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → 𝑤 = 𝑡))) |
36 | 35 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 𝑤 = 〈“𝐴𝑑𝐵”〉) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))) |
37 | 36 | exp4b 632 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝑡 = 〈“𝐴𝑐𝐵”〉 → (𝑤 = 〈“𝐴𝑑𝐵”〉 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))))) |
38 | 37 | com13 88 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 〈“𝐴𝑐𝐵”〉 → (〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝑤 = 〈“𝐴𝑑𝐵”〉 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))))) |
39 | 38 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝑤 = 〈“𝐴𝑑𝐵”〉 → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡)))) |
40 | 39 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈“𝐴𝑑𝐵”〉 → (〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡)))) |
41 | 40 | imp 445 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → 𝑤 = 𝑡))) |
42 | 41 | com13 88 |
. . . . . . . . . . . . . 14
⊢
(((〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑑 = 𝑐) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
43 | 24, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦)) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
44 | 43 | expcom 451 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑉 ((〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐴𝑦𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑥 = 𝑦) → ((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)))) |
45 | 13, 44 | simplbiim 659 |
. . . . . . . . . . 11
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)))) |
46 | 45 | impl 650 |
. . . . . . . . . 10
⊢
(((∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑑 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → ((𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
47 | 46 | rexlimdva 3031 |
. . . . . . . . 9
⊢
((∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑑 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
48 | 47 | com23 86 |
. . . . . . . 8
⊢
((∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑑 ∈ 𝑉) → ((𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
49 | 48 | rexlimdva 3031 |
. . . . . . 7
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡))) |
50 | 49 | impd 447 |
. . . . . 6
⊢
(∃!𝑥 ∈
𝑉 〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) → 𝑤 = 𝑡)) |
51 | 10, 50 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((∃𝑑 ∈ 𝑉 (𝑤 = 〈“𝐴𝑑𝐵”〉 ∧ 〈“𝐴𝑑𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) ∧ ∃𝑐 ∈ 𝑉 (𝑡 = 〈“𝐴𝑐𝐵”〉 ∧ 〈“𝐴𝑐𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) → 𝑤 = 𝑡)) |
52 | 9, 51 | sylbid 230 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)) |
53 | 52 | alrimivv 1856 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∀𝑤∀𝑡((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)) |
54 | | eqeuel 3941 |
. . 3
⊢ (((𝐴(2 WWalksNOn 𝐺)𝐵) ≠ ∅ ∧ ∀𝑤∀𝑡((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 𝑡 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → 𝑤 = 𝑡)) → ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
55 | 2, 53, 54 | syl2anc 693 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
56 | | ovex 6678 |
. . 3
⊢ (𝐴(2 WWalksNOn 𝐺)𝐵) ∈ V |
57 | | euhash1 13208 |
. . 3
⊢ ((𝐴(2 WWalksNOn 𝐺)𝐵) ∈ V → ((#‘(𝐴(2 WWalksNOn 𝐺)𝐵)) = 1 ↔ ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
58 | 56, 57 | mp1i 13 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((#‘(𝐴(2 WWalksNOn 𝐺)𝐵)) = 1 ↔ ∃!𝑤 𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
59 | 55, 58 | mpbird 247 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (#‘(𝐴(2 WWalksNOn 𝐺)𝐵)) = 1) |