| Step | Hyp | Ref
| Expression |
| 1 | | simp3l 1202 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → 𝑃 ∈ 𝑋) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 3 | 2 | wwlks2onv 29973 |
. . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ 〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
| 4 | 1, 3 | sylan 580 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
| 5 | | simp3r 1203 |
. . . . . . . 8
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → 𝑄 ∈ 𝑌) |
| 6 | 2 | wwlks2onv 29973 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑌 ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) |
| 7 | 5, 6 | sylan 580 |
. . . . . . 7
⊢ (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) |
| 8 | | frgrusgr 30280 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
USGraph) |
| 9 | | usgrumgr 29198 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UMGraph) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
UMGraph) |
| 11 | 10 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → 𝐺 ∈ UMGraph) |
| 12 | | simpr3 1197 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) → 𝐵 ∈ (Vtx‘𝐺)) |
| 13 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) → 𝑄 ∈ (Vtx‘𝐺)) |
| 14 | | simpr1 1195 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) → 𝐴 ∈ (Vtx‘𝐺)) |
| 15 | 12, 13, 14 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) |
| 16 | 2 | wwlks2onsym 29978 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UMGraph ∧ (𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺))) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) ↔ 〈“𝐴𝑄𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 17 | 11, 15, 16 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) ↔ 〈“𝐴𝑄𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 18 | | simpr1 1195 |
. . . . . . . . . . . . . 14
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → 𝐺 ∈ FriendGraph ) |
| 19 | | 3simpb 1150 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
| 20 | 19 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
| 21 | | simpr2 1196 |
. . . . . . . . . . . . . 14
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → 𝐴 ≠ 𝐵) |
| 22 | 2 | frgr2wwlkeu 30346 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ 𝐴 ≠ 𝐵) → ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
| 23 | 18, 20, 21, 22 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) |
| 24 | | s3eq2 14909 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑄 → 〈“𝐴𝑥𝐵”〉 = 〈“𝐴𝑄𝐵”〉) |
| 25 | 24 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑄 → (〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑄𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 26 | 25 | riota2 7413 |
. . . . . . . . . . . . . . 15
⊢ ((𝑄 ∈ (Vtx‘𝐺) ∧ ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑄𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑄)) |
| 27 | 26 | ad4ant14 752 |
. . . . . . . . . . . . . 14
⊢ ((((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) ∧ ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑄𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑄)) |
| 28 | | simplr2 1217 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → 𝑃 ∈ (Vtx‘𝐺)) |
| 29 | | s3eq2 14909 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑃 → 〈“𝐴𝑥𝐵”〉 = 〈“𝐴𝑃𝐵”〉) |
| 30 | 29 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑃 → (〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ 〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))) |
| 31 | 30 | riota2 7413 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (Vtx‘𝐺) ∧ ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑃)) |
| 32 | 28, 31 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) ∧ ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑃)) |
| 33 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . 17
⊢
(((℩𝑥
∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑄 ∧ (℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑃) → 𝑄 = 𝑃) |
| 34 | 33 | expcom 413 |
. . . . . . . . . . . . . . . 16
⊢
((℩𝑥
∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑃 → ((℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑄 → 𝑄 = 𝑃)) |
| 35 | 32, 34 | biimtrdi 253 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) ∧ ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑄 → 𝑄 = 𝑃))) |
| 36 | 35 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) ∧ ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((℩𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) = 𝑄 → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃))) |
| 37 | 27, 36 | sylbid 240 |
. . . . . . . . . . . . 13
⊢ ((((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) ∧ ∃!𝑥 ∈ (Vtx‘𝐺)〈“𝐴𝑥𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐴𝑄𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃))) |
| 38 | 23, 37 | mpdan 687 |
. . . . . . . . . . . 12
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (〈“𝐴𝑄𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃))) |
| 39 | 17, 38 | sylbid 240 |
. . . . . . . . . . 11
⊢ (((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) ∧ (𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌))) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃))) |
| 40 | 39 | expimpd 453 |
. . . . . . . . . 10
⊢ ((𝑄 ∈ (Vtx‘𝐺) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) → (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃))) |
| 41 | 40 | ex 412 |
. . . . . . . . 9
⊢ (𝑄 ∈ (Vtx‘𝐺) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃)))) |
| 42 | 41 | com23 86 |
. . . . . . . 8
⊢ (𝑄 ∈ (Vtx‘𝐺) → (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃)))) |
| 43 | 42 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐵 ∈ (Vtx‘𝐺) ∧ 𝑄 ∈ (Vtx‘𝐺) ∧ 𝐴 ∈ (Vtx‘𝐺)) → (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃)))) |
| 44 | 7, 43 | mpcom 38 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃))) |
| 45 | 44 | ex 412 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → 𝑄 = 𝑃)))) |
| 46 | 45 | com24 95 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → (〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → 𝑄 = 𝑃)))) |
| 47 | 46 | imp 406 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝑃 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → 𝑄 = 𝑃))) |
| 48 | 4, 47 | mpd 15 |
. 2
⊢ (((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) ∧ 〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵)) → (〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴) → 𝑄 = 𝑃)) |
| 49 | 48 | expimpd 453 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → ((〈“𝐴𝑃𝐵”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ 〈“𝐵𝑄𝐴”〉 ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → 𝑄 = 𝑃)) |