Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | wwlks2onv 41158 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ 〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
3 | 2 | ex 449 |
. . . . . . 7
⊢ (𝑃 ∈ 𝑋 → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)))) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)))) |
5 | 4 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)))) |
6 | 1 | wwlks2onv 41158 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑌 ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) |
7 | 6 | ex 449 |
. . . . . . 7
⊢ (𝑄 ∈ 𝑌 → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺)))) |
8 | 7 | adantl 481 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺)))) |
9 | 8 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺)))) |
10 | 5, 9 | anim12d 584 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → ((〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))))) |
11 | 10 | imp 444 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴))) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺)))) |
12 | | frgrusgr 41432 |
. . . . . . . . 9
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
13 | | usgrumgr 40409 |
. . . . . . . . 9
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph
) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ UMGraph
) |
15 | 14 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → 𝐺 ∈ UMGraph ) |
16 | | simpl 472 |
. . . . . . 7
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
17 | | eqid 2610 |
. . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
18 | 1, 17 | umgrwwlks2on 41161 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)))) |
19 | 15, 16, 18 | syl2anr 494 |
. . . . . 6
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ ({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)))) |
20 | | simpr 476 |
. . . . . . 7
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) |
21 | 1, 17 | umgrwwlks2on 41161 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) ↔ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺)))) |
22 | 15, 20, 21 | syl2anr 494 |
. . . . . 6
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) ↔ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺)))) |
23 | 19, 22 | anbi12d 743 |
. . . . 5
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → ((〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) ↔ (({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))))) |
24 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → 𝐺 ∈ FriendGraph ) |
25 | 24 | adantl 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → 𝐺 ∈ FriendGraph ) |
26 | | simpll1 1093 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → 𝐴 ∈ (Vtx‘𝐺)) |
27 | | simpll3 1095 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → 𝐵 ∈ (Vtx‘𝐺)) |
28 | | simpr2 1061 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → 𝐴 ≠ 𝐵) |
29 | 26, 27, 28 | 3jca 1235 |
. . . . . . 7
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐴 ≠ 𝐵)) |
30 | 1, 17 | frcond2 41439 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph →
((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐴 ≠ 𝐵) → ∃!𝑝 ∈ (Vtx‘𝐺)({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)))) |
31 | 25, 29, 30 | sylc 63 |
. . . . . 6
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → ∃!𝑝 ∈ (Vtx‘𝐺)({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺))) |
32 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → {𝐴, 𝑝} = {𝐴, 𝑞}) |
33 | 32 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → ({𝐴, 𝑝} ∈ (Edg‘𝐺) ↔ {𝐴, 𝑞} ∈ (Edg‘𝐺))) |
34 | | preq1 4212 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → {𝑝, 𝐵} = {𝑞, 𝐵}) |
35 | 34 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → ({𝑝, 𝐵} ∈ (Edg‘𝐺) ↔ {𝑞, 𝐵} ∈ (Edg‘𝐺))) |
36 | 33, 35 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → (({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ↔ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺)))) |
37 | 36 | reu4 3367 |
. . . . . . 7
⊢
(∃!𝑝 ∈
(Vtx‘𝐺)({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ↔ (∃𝑝 ∈ (Vtx‘𝐺)({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞))) |
38 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑃 → {𝐴, 𝑝} = {𝐴, 𝑃}) |
39 | 38 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 𝑃 → ({𝐴, 𝑝} ∈ (Edg‘𝐺) ↔ {𝐴, 𝑃} ∈ (Edg‘𝐺))) |
40 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑃 → {𝑝, 𝐵} = {𝑃, 𝐵}) |
41 | 40 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 𝑃 → ({𝑝, 𝐵} ∈ (Edg‘𝐺) ↔ {𝑃, 𝐵} ∈ (Edg‘𝐺))) |
42 | 39, 41 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑃 → (({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ↔ ({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)))) |
43 | 42 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑃 → ((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) ↔ (({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))))) |
44 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑃 → (𝑝 = 𝑞 ↔ 𝑃 = 𝑞)) |
45 | 43, 44 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑃 → (((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) ↔ ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑃 = 𝑞))) |
46 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 = 𝑄 → {𝐴, 𝑞} = {𝐴, 𝑄}) |
47 | 46 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 = 𝑄 → ({𝐴, 𝑞} ∈ (Edg‘𝐺) ↔ {𝐴, 𝑄} ∈ (Edg‘𝐺))) |
48 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 = 𝑄 → {𝑞, 𝐵} = {𝑄, 𝐵}) |
49 | 48 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 = 𝑄 → ({𝑞, 𝐵} ∈ (Edg‘𝐺) ↔ {𝑄, 𝐵} ∈ (Edg‘𝐺))) |
50 | 47, 49 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 𝑄 → (({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺)) ↔ ({𝐴, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐵} ∈ (Edg‘𝐺)))) |
51 | 50 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 𝑄 → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) ↔ (({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐵} ∈ (Edg‘𝐺))))) |
52 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 𝑄 → (𝑃 = 𝑞 ↔ 𝑃 = 𝑄)) |
53 | 51, 52 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = 𝑄 → (((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑃 = 𝑞) ↔ ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐵} ∈ (Edg‘𝐺))) → 𝑃 = 𝑄))) |
54 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝐴, 𝑄} = {𝑄, 𝐴} |
55 | 54 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝐴, 𝑄} ∈ (Edg‘𝐺) ↔ {𝑄, 𝐴} ∈ (Edg‘𝐺)) |
56 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑄, 𝐵} = {𝐵, 𝑄} |
57 | 56 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑄, 𝐵} ∈ (Edg‘𝐺) ↔ {𝐵, 𝑄} ∈ (Edg‘𝐺)) |
58 | 55, 57 | anbi12ci 730 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝐴, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐵} ∈ (Edg‘𝐺)) ↔ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) |
59 | 58 | anbi2i 726 |
. . . . . . . . . . . . . . . . 17
⊢ ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐵} ∈ (Edg‘𝐺))) ↔ (({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺)))) |
60 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 = 𝑄 ↔ 𝑄 = 𝑃) |
61 | 59, 60 | imbi12i 339 |
. . . . . . . . . . . . . . . 16
⊢
(((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐵} ∈ (Edg‘𝐺))) → 𝑃 = 𝑄) ↔ ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃)) |
62 | 53, 61 | syl6bb 275 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑄 → (((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑃 = 𝑞) ↔ ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃))) |
63 | 45, 62 | rspc2v 3293 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺)) → (∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃))) |
64 | 63 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (Vtx‘𝐺) → (𝑄 ∈ (Vtx‘𝐺) → (∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃)))) |
65 | 64 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (𝑄 ∈ (Vtx‘𝐺) → (∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃)))) |
66 | 65 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑄 ∈ (Vtx‘𝐺) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃)))) |
67 | 66 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃)))) |
68 | 67 | impcom 445 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) → (∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃))) |
69 | 68 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (∀𝑝 ∈ (Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃))) |
70 | 69 | com12 32 |
. . . . . . 7
⊢
(∀𝑝 ∈
(Vtx‘𝐺)∀𝑞 ∈ (Vtx‘𝐺)((({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐴, 𝑞} ∈ (Edg‘𝐺) ∧ {𝑞, 𝐵} ∈ (Edg‘𝐺))) → 𝑝 = 𝑞) → ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃))) |
71 | 37, 70 | simplbiim 657 |
. . . . . 6
⊢
(∃!𝑝 ∈
(Vtx‘𝐺)({𝐴, 𝑝} ∈ (Edg‘𝐺) ∧ {𝑝, 𝐵} ∈ (Edg‘𝐺)) → ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃))) |
72 | 31, 71 | mpcom 37 |
. . . . 5
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → ((({𝐴, 𝑃} ∈ (Edg‘𝐺) ∧ {𝑃, 𝐵} ∈ (Edg‘𝐺)) ∧ ({𝐵, 𝑄} ∈ (Edg‘𝐺) ∧ {𝑄, 𝐴} ∈ (Edg‘𝐺))) → 𝑄 = 𝑃)) |
73 | 23, 72 | sylbid 229 |
. . . 4
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → ((〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → 𝑄 = 𝑃)) |
74 | 73 | expimpd 627 |
. . 3
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) → (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴))) → 𝑄 = 𝑃)) |
75 | 11, 74 | mpcom 37 |
. 2
⊢ (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴))) → 𝑄 = 𝑃) |
76 | 75 | ex 449 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → ((〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → 𝑄 = 𝑃)) |