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 biimtrdi ⊢ ( ( ( ( 𝑄 ∈ ( 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 𝐺 ) 𝐴 ) ) → 𝑄 = 𝑃 ) )