Theorem frgr2wwlkeu

Description: For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 4-Jan-2022)

	Ref	Expression
Hypothesis	frgr2wwlkeu.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	frgr2wwlkeu	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		df-3an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) )
3		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4	1 3	frcond2	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
5	2 4	biimtrrid	⊢ ( 𝐺 ∈ FriendGraph → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
6	5	3impib	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) )
7		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
8		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
9		3anan32	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) )
10	1 3	umgrwwlks2on	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
11	10	ex	⊢ ( 𝐺 ∈ UMGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
12	9 11	biimtrrid	⊢ ( 𝐺 ∈ UMGraph → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
13	7 8 12	3syl	⊢ ( 𝐺 ∈ FriendGraph → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
14	13	impl	⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
15	14	reubidva	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( ∃! 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ∃! 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
16	15	3adant3	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ∃! 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ∃! 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) ) )
17	6 16	mpbird	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑐 ∈ 𝑉 ⟨“ 𝐴 𝑐 𝐵 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )