Step |
Hyp |
Ref |
Expression |
1 |
|
simp3l |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) → 𝑃 ∈ 𝑋 ) |
2 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
3 |
2
|
wwlks2onv |
⊢ ( ( 𝑃 ∈ 𝑋 ∧ 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
4 |
1 3
|
sylan |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
5 |
|
simp3r |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) → 𝑄 ∈ 𝑌 ) |
6 |
2
|
wwlks2onv |
⊢ ( ( 𝑄 ∈ 𝑌 ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
7 |
5 6
|
sylan |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
8 |
|
frgrusgr |
⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph ) |
9 |
|
usgrumgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph ) |
10 |
8 9
|
syl |
⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ UMGraph ) |
11 |
10
|
3ad2ant1 |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) → 𝐺 ∈ UMGraph ) |
12 |
|
simpr3 |
⊢ ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) |
13 |
|
simpl |
⊢ ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑄 ∈ ( Vtx ‘ 𝐺 ) ) |
14 |
|
simpr1 |
⊢ ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) |
15 |
12 13 14
|
3jca |
⊢ ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
16 |
2
|
wwlks2onsym |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ↔ 〈“ 𝐴 𝑄 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) |
17 |
11 15 16
|
syl2anr |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → ( 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ↔ 〈“ 𝐴 𝑄 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) |
18 |
|
simpr1 |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → 𝐺 ∈ FriendGraph ) |
19 |
|
3simpb |
⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
20 |
19
|
ad2antlr |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
21 |
|
simpr2 |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → 𝐴 ≠ 𝐵 ) |
22 |
2
|
frgr2wwlkeu |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) |
23 |
18 20 21 22
|
syl3anc |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) |
24 |
|
s3eq2 |
⊢ ( 𝑥 = 𝑄 → 〈“ 𝐴 𝑥 𝐵 ”〉 = 〈“ 𝐴 𝑄 𝐵 ”〉 ) |
25 |
24
|
eleq1d |
⊢ ( 𝑥 = 𝑄 → ( 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ 〈“ 𝐴 𝑄 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) |
26 |
25
|
riota2 |
⊢ ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 〈“ 𝐴 𝑄 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑄 ) ) |
27 |
26
|
ad4ant14 |
⊢ ( ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) ∧ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 〈“ 𝐴 𝑄 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑄 ) ) |
28 |
|
simplr2 |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → 𝑃 ∈ ( Vtx ‘ 𝐺 ) ) |
29 |
|
s3eq2 |
⊢ ( 𝑥 = 𝑃 → 〈“ 𝐴 𝑥 𝐵 ”〉 = 〈“ 𝐴 𝑃 𝐵 ”〉 ) |
30 |
29
|
eleq1d |
⊢ ( 𝑥 = 𝑃 → ( 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) |
31 |
30
|
riota2 |
⊢ ( ( 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑃 ) ) |
32 |
28 31
|
sylan |
⊢ ( ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) ∧ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑃 ) ) |
33 |
|
eqtr2 |
⊢ ( ( ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑄 ∧ ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑃 ) → 𝑄 = 𝑃 ) |
34 |
33
|
expcom |
⊢ ( ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑃 → ( ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑄 → 𝑄 = 𝑃 ) ) |
35 |
32 34
|
syl6bi |
⊢ ( ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) ∧ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑄 → 𝑄 = 𝑃 ) ) ) |
36 |
35
|
com23 |
⊢ ( ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) ∧ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( ℩ 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 𝑄 → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) |
37 |
27 36
|
sylbid |
⊢ ( ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) ∧ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) 〈“ 𝐴 𝑥 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 〈“ 𝐴 𝑄 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) |
38 |
23 37
|
mpdan |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → ( 〈“ 𝐴 𝑄 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) |
39 |
17 38
|
sylbid |
⊢ ( ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ) → ( 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) |
40 |
39
|
expimpd |
⊢ ( ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) |
41 |
40
|
ex |
⊢ ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) ) |
42 |
41
|
com23 |
⊢ ( 𝑄 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) ) |
43 |
42
|
3ad2ant2 |
⊢ ( ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑄 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) ) |
44 |
7 43
|
mpcom |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) |
45 |
44
|
ex |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) → ( 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → 𝑄 = 𝑃 ) ) ) ) |
46 |
45
|
com24 |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) → ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) → 𝑄 = 𝑃 ) ) ) ) |
47 |
46
|
imp |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) → 𝑄 = 𝑃 ) ) ) |
48 |
4 47
|
mpd |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) ∧ 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) → 𝑄 = 𝑃 ) ) |
49 |
48
|
expimpd |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) ) → ( ( 〈“ 𝐴 𝑃 𝐵 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 〈“ 𝐵 𝑄 𝐴 ”〉 ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → 𝑄 = 𝑃 ) ) |