Theorem frgr2wwlkn0

Description: In a friendship graph, there is always a path/walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021)

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

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	frgr2wwlkeu	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
3		reurex	⊢ ( ∃! 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ∃ 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )
4		ne0i	⊢ ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ≠ ∅ )
5	4	rexlimivw	⊢ ( ∃ 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) → ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ≠ ∅ )
6	2 3 5	3syl	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ≠ ∅ )