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	⊢ ∀ 𝑘 ∈ ∅ ∀ 𝑙 ∈ ( ∅ ∖ { 𝑘 } ) ∃! 𝑥 ∈ ∅ { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ ∅ )
3		vtxval0	⊢ ( Vtx ‘ ∅ ) = ∅
4	3	eqcomi	⊢ ∅ = ( Vtx ‘ ∅ )
5		eqid	⊢ ( Edg ‘ ∅ ) = ( Edg ‘ ∅ )
6	4 5	isfrgr	⊢ ( ∅ ∈ FriendGraph ↔ ( ∅ ∈ USGraph ∧ ∀ 𝑘 ∈ ∅ ∀ 𝑙 ∈ ( ∅ ∖ { 𝑘 } ) ∃! 𝑥 ∈ ∅ { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ ∅ ) ) )
7	1 2 6	mpbir2an	⊢ ∅ ∈ FriendGraph