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 ⊢ V = Vtx ⁡ G
frcond1.e ⊢ E = Edg ⁡ G
Assertion frcond2 ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b ∈ E ∧ b C ∈ E

Proof

Step Hyp Ref Expression
1 frcond1.v ⊢ V = Vtx ⁡ G
2 frcond1.e ⊢ E = Edg ⁡ G
3 1 2 frcond1 ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b b C ⊆ E
4 prex ⊢ A b ∈ V
5 prex ⊢ b C ∈ V
6 4 5 prss ⊢ A b ∈ E ∧ b C ∈ E ↔ A b b C ⊆ E
7 6 bicomi ⊢ A b b C ⊆ E ↔ A b ∈ E ∧ b C ∈ E
8 7 reubii ⊢ ∃! b ∈ V A b b C ⊆ E ↔ ∃! b ∈ V A b ∈ E ∧ b C ∈ E
9 3 8 imbitrdi ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b ∈ E ∧ b C ∈ E