Metamath Proof Explorer

Theorem frgreu

Description: Variant of frcond2 : Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 4-Jan-2022)

Ref Expression
Hypotheses frcond1.v ⊢ V = Vtx ⁡ G
frcond1.e ⊢ E = Edg ⁡ G
Assertion frgreu ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b 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 frcond2 ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b ∈ E ∧ b C ∈ E
4 3 imp ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b ∈ E ∧ b C ∈ E
5 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
6 5 adantr ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → G ∈ USGraph
7 simpl ⊢ A b ∈ E ∧ b C ∈ E → A b ∈ E
8 2 1 usgrpredgv ⊢ G ∈ USGraph ∧ A b ∈ E → A ∈ V ∧ b ∈ V
9 8 simprd ⊢ G ∈ USGraph ∧ A b ∈ E → b ∈ V
10 6 7 9 syl2an ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E → b ∈ V
11 10 reueubd ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b ∈ E ∧ b C ∈ E ↔ ∃! b A b ∈ E ∧ b C ∈ E
12 4 11 mpbid ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b A b ∈ E ∧ b C ∈ E
13 12 ex ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b A b ∈ E ∧ b C ∈ E