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 ∈ ∅ x k x l ⊆ Edg ⁡ ∅
3 vtxval0 ⊢ Vtx ⁡ ∅ = ∅
4 3 eqcomi ⊢ ∅ = Vtx ⁡ ∅
5 eqid ⊢ Edg ⁡ ∅ = Edg ⁡ ∅
6 4 5 isfrgr ⊢ ∅ ∈ FriendGraph ↔ ∅ ∈ USGraph ∧ ∀ k ∈ ∅ ∀ l ∈ ∅ ∖ k ∃! x ∈ ∅ x k x l ⊆ Edg ⁡ ∅
7 1 2 6 mpbir2an ⊢ ∅ ∈ FriendGraph