Metamath Proof Explorer


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 syl6ib ( 𝐺 ∈ FriendGraph → ( ( 𝐴𝑉𝐶𝑉𝐴𝐶 ) → ∃! 𝑏𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )