Metamath Proof Explorer

Theorem frgr0

Description: The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021)

Ref Expression
Assertion frgr0 ⊢∅∈FriendGraph

Proof

Step Hyp Ref Expression
1 usgr0 ⊢∅∈USGraph
2 ral0 ⊢∀k∈∅∀l∈∅∖k∃!x∈∅xkxl⊆Edg⁡∅
3 vtxval0 ⊢Vtx⁡∅=∅
4 3 eqcomi ⊢∅=Vtx⁡∅
5 eqid ⊢Edg⁡∅=Edg⁡∅
6 4 5 isfrgr ⊢∅∈FriendGraph↔∅∈USGraph∧∀k∈∅∀l∈∅∖k∃!x∈∅xkxl⊆Edg⁡∅
7 1 2 6 mpbir2an ⊢∅∈FriendGraph