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→∃!bAb∈E∧bC∈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∈VAb∈E∧bC∈E
4 3 imp ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃!b∈VAb∈E∧bC∈E
5 frgrusgr ⊢G∈FriendGraph→G∈USGraph
6 5 adantr ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→G∈USGraph
7 simpl ⊢Ab∈E∧bC∈E→Ab∈E
8 2 1 usgrpredgv ⊢G∈USGraph∧Ab∈E→A∈V∧b∈V
9 8 simprd ⊢G∈USGraph∧Ab∈E→b∈V
10 6 7 9 syl2an ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧Ab∈E∧bC∈E→b∈V
11 10 reueubd ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃!b∈VAb∈E∧bC∈E↔∃!bAb∈E∧bC∈E
12 4 11 mpbid ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃!bAb∈E∧bC∈E
13 12 ex ⊢G∈FriendGraph→A∈V∧C∈V∧A≠C→∃!bAb∈E∧bC∈E