Theorem frcond2

Description: The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021)

	Ref	Expression
Hypotheses	frcond1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frcond1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	frcond2	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frcond1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frcond1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	frcond1	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )
4		prex	⊢ { 𝐴 , 𝑏 } ∈ V
5		prex	⊢ { 𝑏 , 𝐶 } ∈ V
6	4 5	prss	⊢ ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ↔ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 )
7	6	bicomi	⊢ ( { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) )
8	7	reubii	⊢ ( ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ↔ ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) )
9	3 8	imbitrdi	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )