Metamath Proof Explorer

Theorem 1to3vfriendship

Description: The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ⊢ V = Vtx ⁡ G
3vfriswmgr.e ⊢ E = Edg ⁡ G
Assertion 1to3vfriendship ⊢ A ∈ X ∧ V = A ∨ V = A B ∨ V = A B C → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢ V = Vtx ⁡ G
2 3vfriswmgr.e ⊢ E = Edg ⁡ G
3 1 2 1to3vfriswmgr ⊢ A ∈ X ∧ V = A ∨ V = A B ∨ V = A B C → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v w v ∈ E ∧ ∃! x ∈ V ∖ v w x ∈ E
4 prcom ⊢ w v = v w
5 4 eleq1i ⊢ w v ∈ E ↔ v w ∈ E
6 5 birani ⊢ w v ∈ E ∧ ∃! x ∈ V ∖ v w x ∈ E → v w ∈ E
7 6 ralimi ⊢ ∀ w ∈ V ∖ v w v ∈ E ∧ ∃! x ∈ V ∖ v w x ∈ E → ∀ w ∈ V ∖ v v w ∈ E
8 7 reximi ⊢ ∃ v ∈ V ∀ w ∈ V ∖ v w v ∈ E ∧ ∃! x ∈ V ∖ v w x ∈ E → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
9 3 8 syl6 ⊢ A ∈ X ∧ V = A ∨ V = A B ∨ V = A B C → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E