Theorem frcond4

Description: The friendship condition, alternatively expressed by neighborhoods: in a friendship graph, the neighborhoods of two different vertices have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021) (Proof shortened by AV, 30-Dec-2021)

	Ref	Expression
Hypotheses	frcond1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frcond1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	frcond4	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		frcond1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frcond1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	frcond3	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑘 ∈ 𝑉 ∧ 𝑙 ∈ 𝑉 ∧ 𝑘 ≠ 𝑙 ) → ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } ) )
4		eldifsn	⊢ ( 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ↔ ( 𝑙 ∈ 𝑉 ∧ 𝑙 ≠ 𝑘 ) )
5		necom	⊢ ( 𝑙 ≠ 𝑘 ↔ 𝑘 ≠ 𝑙 )
6	5	biimpi	⊢ ( 𝑙 ≠ 𝑘 → 𝑘 ≠ 𝑙 )
7	6	anim2i	⊢ ( ( 𝑙 ∈ 𝑉 ∧ 𝑙 ≠ 𝑘 ) → ( 𝑙 ∈ 𝑉 ∧ 𝑘 ≠ 𝑙 ) )
8	4 7	sylbi	⊢ ( 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) → ( 𝑙 ∈ 𝑉 ∧ 𝑘 ≠ 𝑙 ) )
9	8	anim2i	⊢ ( ( 𝑘 ∈ 𝑉 ∧ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ) → ( 𝑘 ∈ 𝑉 ∧ ( 𝑙 ∈ 𝑉 ∧ 𝑘 ≠ 𝑙 ) ) )
10		3anass	⊢ ( ( 𝑘 ∈ 𝑉 ∧ 𝑙 ∈ 𝑉 ∧ 𝑘 ≠ 𝑙 ) ↔ ( 𝑘 ∈ 𝑉 ∧ ( 𝑙 ∈ 𝑉 ∧ 𝑘 ≠ 𝑙 ) ) )
11	9 10	sylibr	⊢ ( ( 𝑘 ∈ 𝑉 ∧ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ) → ( 𝑘 ∈ 𝑉 ∧ 𝑙 ∈ 𝑉 ∧ 𝑘 ≠ 𝑙 ) )
12	3 11	impel	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑘 ∈ 𝑉 ∧ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ) ) → ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } )
13	12	ralrimivva	⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } )