Metamath Proof Explorer

Theorem frgr2wwlk1

Description: In a friendship graph, there is exactly one walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Revised by AV, 13-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypothesis frgr2wwlkeu.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion frgr2wwlk1 ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 frgr2wwlkeu.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 frgr2wwlkn0 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ≠ ∅ )
3 1 elwwlks2ons3 ⊢ ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ∃ 𝑑 ∈ 𝑉 ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
4 1 elwwlks2ons3 ⊢ ( 𝑡 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ∃ 𝑐 ∈ 𝑉 ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
5 3 4 anbi12i ⊢ ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 𝑡 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ↔ ( ∃ 𝑑 ∈ 𝑉 ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ∧ ∃ 𝑐 ∈ 𝑉 ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) )
6 1 frgr2wwlkeu ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
7 s3eq2 ⊢ ( 𝑥 = 𝑦 → ⟨“ 𝐴 𝑥 𝐵 ”⟩ = ⟨“ 𝐴 𝑦 𝐵 ”⟩ )
8 7 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
9 8 reu4 ⊢ ( ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑥 = 𝑦 ) ) )
10 s3eq2 ⊢ ( 𝑥 = 𝑑 → ⟨“ 𝐴 𝑥 𝐵 ”⟩ = ⟨“ 𝐴 𝑑 𝐵 ”⟩ )
11 10 eleq1d ⊢ ( 𝑥 = 𝑑 → ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
12 11 anbi1d ⊢ ( 𝑥 = 𝑑 → ( ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ↔ ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) )
13 equequ1 ⊢ ( 𝑥 = 𝑑 → ( 𝑥 = 𝑦 ↔ 𝑑 = 𝑦 ) )
14 12 13 imbi12d ⊢ ( 𝑥 = 𝑑 → ( ( ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑥 = 𝑦 ) ↔ ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑦 ) ) )
15 s3eq2 ⊢ ( 𝑦 = 𝑐 → ⟨“ 𝐴 𝑦 𝐵 ”⟩ = ⟨“ 𝐴 𝑐 𝐵 ”⟩ )
16 15 eleq1d ⊢ ( 𝑦 = 𝑐 → ( ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
17 16 anbi2d ⊢ ( 𝑦 = 𝑐 → ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ↔ ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) )
18 equequ2 ⊢ ( 𝑦 = 𝑐 → ( 𝑑 = 𝑦 ↔ 𝑑 = 𝑐 ) )
19 17 18 imbi12d ⊢ ( 𝑦 = 𝑐 → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑦 ) ↔ ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) ) )
20 14 19 rspc2va ⊢ ( ( ( 𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑥 = 𝑦 ) ) → ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) )
21 pm3.35 ⊢ ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ∧ ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) ) → 𝑑 = 𝑐 )
22 s3eq2 ⊢ ( 𝑐 = 𝑑 → ⟨“ 𝐴 𝑐 𝐵 ”⟩ = ⟨“ 𝐴 𝑑 𝐵 ”⟩ )
23 22 equcoms ⊢ ( 𝑑 = 𝑐 → ⟨“ 𝐴 𝑐 𝐵 ”⟩ = ⟨“ 𝐴 𝑑 𝐵 ”⟩ )
24 23 adantr ⊢ ( ( 𝑑 = 𝑐 ∧ ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) ) → ⟨“ 𝐴 𝑐 𝐵 ”⟩ = ⟨“ 𝐴 𝑑 𝐵 ”⟩ )
25 eqeq12 ⊢ ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) → ( 𝑡 = 𝑤 ↔ ⟨“ 𝐴 𝑐 𝐵 ”⟩ = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) )
26 25 adantl ⊢ ( ( 𝑑 = 𝑐 ∧ ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) ) → ( 𝑡 = 𝑤 ↔ ⟨“ 𝐴 𝑐 𝐵 ”⟩ = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) )
27 24 26 mpbird ⊢ ( ( 𝑑 = 𝑐 ∧ ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) ) → 𝑡 = 𝑤 )
28 27 equcomd ⊢ ( ( 𝑑 = 𝑐 ∧ ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) ) → 𝑤 = 𝑡 )
29 28 ex ⊢ ( 𝑑 = 𝑐 → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) → 𝑤 = 𝑡 ) )
30 21 29 syl ⊢ ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ∧ ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) → 𝑤 = 𝑡 ) )
31 30 ex ⊢ ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) → 𝑤 = 𝑡 ) ) )
32 31 com23 ⊢ ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ) → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → 𝑤 = 𝑡 ) ) )
33 32 exp4b ⊢ ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ → ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → 𝑤 = 𝑡 ) ) ) ) )
34 33 com13 ⊢ ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ → ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → 𝑤 = 𝑡 ) ) ) ) )
35 34 imp ⊢ ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → 𝑤 = 𝑡 ) ) ) )
36 35 com13 ⊢ ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ → ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → 𝑤 = 𝑡 ) ) ) )
37 36 imp ⊢ ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → 𝑤 = 𝑡 ) ) )
38 37 com13 ⊢ ( ( ( ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑑 = 𝑐 ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) )
39 20 38 syl ⊢ ( ( ( 𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑥 = 𝑦 ) ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) )
40 39 expcom ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ⟨“ 𝐴 𝑦 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑥 = 𝑦 ) → ( ( 𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) ) )
41 9 40 simplbiim ⊢ ( ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ( 𝑑 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) ) )
42 41 impl ⊢ ( ( ( ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 𝑑 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) )
43 42 rexlimdva ⊢ ( ( ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 𝑑 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝑉 ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) )
44 43 com23 ⊢ ( ( ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 𝑑 ∈ 𝑉 ) → ( ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ∃ 𝑐 ∈ 𝑉 ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) )
45 44 rexlimdva ⊢ ( ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ∃ 𝑑 ∈ 𝑉 ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → ( ∃ 𝑐 ∈ 𝑉 ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) )
46 45 impd ⊢ ( ∃! 𝑥 ∈ 𝑉 ⟨“ 𝐴 𝑥 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( ( ∃ 𝑑 ∈ 𝑉 ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ∧ ∃ 𝑐 ∈ 𝑉 ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) → 𝑤 = 𝑡 ) )
47 6 46 syl ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ∃ 𝑑 ∈ 𝑉 ( 𝑤 = ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑑 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ∧ ∃ 𝑐 ∈ 𝑉 ( 𝑡 = ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∧ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) ) → 𝑤 = 𝑡 ) )
48 5 47 syl5bi ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 𝑡 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) )
49 48 alrimivv ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑤 ∀ 𝑡 ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 𝑡 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) )
50 eqeuel ⊢ ( ( ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ≠ ∅ ∧ ∀ 𝑤 ∀ 𝑡 ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ 𝑡 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) → 𝑤 = 𝑡 ) ) → ∃! 𝑤 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
51 2 49 50 syl2anc ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑤 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
52 ovex ⊢ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∈ V
53 euhash1 ⊢ ( ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∈ V → ( ( ♯ ‘ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 1 ↔ ∃! 𝑤 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
54 52 53 mp1i ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ♯ ‘ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 1 ↔ ∃! 𝑤 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) )
55 51 54 mpbird ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) = 1 )