Theorem uhgr0

Description: The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020)

	Ref	Expression
Assertion	uhgr0	⊢ ∅ ∈ UHGraph

Proof

Step	Hyp	Ref	Expression
1		f0	⊢ ∅ : ∅ ⟶ ∅
2		dm0	⊢ dom ∅ = ∅
3		pw0	⊢ 𝒫 ∅ = { ∅ }
4	3	difeq1i	⊢ ( 𝒫 ∅ ∖ { ∅ } ) = ( { ∅ } ∖ { ∅ } )
5		difid	⊢ ( { ∅ } ∖ { ∅ } ) = ∅
6	4 5	eqtri	⊢ ( 𝒫 ∅ ∖ { ∅ } ) = ∅
7	2 6	feq23i	⊢ ( ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } ) ↔ ∅ : ∅ ⟶ ∅ )
8	1 7	mpbir	⊢ ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } )
9		0ex	⊢ ∅ ∈ V
10		vtxval0	⊢ ( Vtx ‘ ∅ ) = ∅
11	10	eqcomi	⊢ ∅ = ( Vtx ‘ ∅ )
12		iedgval0	⊢ ( iEdg ‘ ∅ ) = ∅
13	12	eqcomi	⊢ ∅ = ( iEdg ‘ ∅ )
14	11 13	isuhgr	⊢ ( ∅ ∈ V → ( ∅ ∈ UHGraph ↔ ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } ) ) )
15	9 14	ax-mp	⊢ ( ∅ ∈ UHGraph ↔ ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } ) )
16	8 15	mpbir	⊢ ∅ ∈ UHGraph