Step | Hyp | Ref
| Expression |
1 | | 2wlkonotv 26404 |
. . . 4
⊢
(〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
2 | | 2wlkonotv 26404 |
. . . 4
⊢
(〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
3 | 1, 2 | anim12i 588 |
. . 3
⊢
((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))) |
4 | | frisusgra 26519 |
. . . . . . . . . . . . 13
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
5 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑉 USGrph 𝐸) |
6 | | simprr3 1104 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → 𝐴 ∈ 𝑉) |
7 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → 𝑃 ∈ 𝑉) |
8 | | simprr1 1102 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → 𝐵 ∈ 𝑉) |
9 | 6, 7, 8 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → (𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
10 | | usg2wlkonot 26410 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸))) |
11 | 5, 9, 10 | syl2anr 494 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → (〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸))) |
12 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
13 | | usg2wlkonot 26410 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) ↔ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸))) |
14 | 5, 12, 13 | syl2anr 494 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → (〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) ↔ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸))) |
15 | 11, 14 | anbi12d 743 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) ↔ (({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)))) |
16 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑉 FriendGrph 𝐸) |
17 | 16 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → 𝑉 FriendGrph 𝐸) |
18 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ 𝑉) |
19 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ 𝑉) |
20 | | necom 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
21 | 20 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴) |
22 | 21 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → 𝐵 ≠ 𝐴) |
23 | 18, 19, 22 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ≠ 𝐴)) |
24 | | frgraeu 26581 |
. . . . . . . . . . . 12
⊢ (𝑉 FriendGrph 𝐸 → ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ≠ 𝐴) → ∃!𝑝({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸))) |
25 | 17, 23, 24 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → ∃!𝑝({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸)) |
26 | | preq2 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑞 → {𝐵, 𝑝} = {𝐵, 𝑞}) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑞 → ({𝐵, 𝑝} ∈ ran 𝐸 ↔ {𝐵, 𝑞} ∈ ran 𝐸)) |
28 | | preq1 4212 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑞 → {𝑝, 𝐴} = {𝑞, 𝐴}) |
29 | 28 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑞 → ({𝑝, 𝐴} ∈ ran 𝐸 ↔ {𝑞, 𝐴} ∈ ran 𝐸)) |
30 | 27, 29 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑞 → (({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ↔ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸))) |
31 | 30 | eu4 2506 |
. . . . . . . . . . . 12
⊢
(∃!𝑝({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ↔ (∃𝑝({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞))) |
32 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 = 𝑃 → {𝐵, 𝑝} = {𝐵, 𝑃}) |
33 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {𝐵, 𝑃} = {𝑃, 𝐵} |
34 | 32, 33 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 = 𝑃 → {𝐵, 𝑝} = {𝑃, 𝐵}) |
35 | 34 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = 𝑃 → ({𝐵, 𝑝} ∈ ran 𝐸 ↔ {𝑃, 𝐵} ∈ ran 𝐸)) |
36 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 = 𝑃 → {𝑝, 𝐴} = {𝑃, 𝐴}) |
37 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {𝑃, 𝐴} = {𝐴, 𝑃} |
38 | 36, 37 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 = 𝑃 → {𝑝, 𝐴} = {𝐴, 𝑃}) |
39 | 38 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = 𝑃 → ({𝑝, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝑃} ∈ ran 𝐸)) |
40 | 35, 39 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = 𝑃 → (({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ↔ ({𝑃, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝑃} ∈ ran 𝐸))) |
41 | | ancom 465 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (({𝑃, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝑃} ∈ ran 𝐸) ↔ ({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸)) |
42 | 40, 41 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = 𝑃 → (({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸))) |
43 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 = 𝑄 → {𝐵, 𝑞} = {𝐵, 𝑄}) |
44 | 43 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 = 𝑄 → ({𝐵, 𝑞} ∈ ran 𝐸 ↔ {𝐵, 𝑄} ∈ ran 𝐸)) |
45 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 = 𝑄 → {𝑞, 𝐴} = {𝑄, 𝐴}) |
46 | 45 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 = 𝑄 → ({𝑞, 𝐴} ∈ ran 𝐸 ↔ {𝑄, 𝐴} ∈ ran 𝐸)) |
47 | 44, 46 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 = 𝑄 → (({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸) ↔ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸))) |
48 | 42, 47 | bi2anan9 913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑄) → ((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) ↔ (({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)))) |
49 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑄) → (𝑝 = 𝑞 ↔ 𝑃 = 𝑄)) |
50 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 = 𝑄 ↔ 𝑄 = 𝑃) |
51 | 49, 50 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑄) → (𝑝 = 𝑞 ↔ 𝑄 = 𝑃)) |
52 | 48, 51 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑄) → (((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) ↔ ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃))) |
53 | 52 | spc2gv 3269 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉) → (∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃))) |
54 | 53 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑄 ∈ 𝑉 → (𝑃 ∈ 𝑉 → (∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃)))) |
55 | 54 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝑃 ∈ 𝑉 → (∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃)))) |
56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝑃 ∈ 𝑉 → (∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃)))) |
57 | 56 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → (∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃))) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → (∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃))) |
59 | 58 | com12 32 |
. . . . . . . . . . . . 13
⊢
(∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞) → (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃))) |
60 | 59 | adantl 481 |
. . . . . . . . . . . 12
⊢
((∃𝑝({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ∀𝑝∀𝑞((({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) ∧ ({𝐵, 𝑞} ∈ ran 𝐸 ∧ {𝑞, 𝐴} ∈ ran 𝐸)) → 𝑝 = 𝑞)) → (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃))) |
61 | 31, 60 | sylbi 206 |
. . . . . . . . . . 11
⊢
(∃!𝑝({𝐵, 𝑝} ∈ ran 𝐸 ∧ {𝑝, 𝐴} ∈ ran 𝐸) → (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃))) |
62 | 25, 61 | mpcom 37 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → ((({𝐴, 𝑃} ∈ ran 𝐸 ∧ {𝑃, 𝐵} ∈ ran 𝐸) ∧ ({𝐵, 𝑄} ∈ ran 𝐸 ∧ {𝑄, 𝐴} ∈ ran 𝐸)) → 𝑄 = 𝑃)) |
63 | 15, 62 | sylbid 229 |
. . . . . . . . 9
⊢ (((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵)) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → 𝑄 = 𝑃)) |
64 | 63 | ex 449 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → 𝑄 = 𝑃))) |
65 | 64 | com23 84 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑉 ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑄 = 𝑃))) |
66 | 65 | ex 449 |
. . . . . 6
⊢ (𝑃 ∈ 𝑉 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑄 = 𝑃)))) |
67 | 66 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑄 = 𝑃)))) |
68 | 67 | adantl 481 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑄 = 𝑃)))) |
69 | 68 | imp 444 |
. . 3
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑄 = 𝑃))) |
70 | 3, 69 | mpcom 37 |
. 2
⊢
((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → 𝑄 = 𝑃)) |
71 | 70 | com12 32 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → 𝑄 = 𝑃)) |