Metamath Proof Explorer


Theorem frgr2wwlkeqm

Description: If there is a (simple) path of length 2 from one vertex to another vertex and a (simple) path of length 2 from the other vertex back to the first vertex in a friendship graph, then the middle vertex is the same. This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 20-Feb-2018) (Revised by AV, 13-May-2021) (Proof shortened by AV, 7-Jan-2022)

Ref Expression
Assertion frgr2wwlkeqm ( ( 𝐺 ∈ FriendGraph ∧ 𝐴𝐵 ∧ ( 𝑃𝑋𝑄𝑌 ) ) → ( ( ⟨“ 𝐴 𝑃 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐵 𝑄 𝐴 ”⟩ ∈ ( 𝐵 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) → 𝑄 = 𝑃 ) )

Proof

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 𝐺 ) 𝐴 ) ) → 𝑄 = 𝑃 ) )