Theorem uhgr0

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

	Ref	Expression
Assertion	uhgr0	$$⊢\varnothing \in \mathrm{UHGraph}$$

Proof

Step	Hyp	Ref	Expression
1		f0	$$⊢\varnothing :\varnothing ⟶\varnothing$$
2		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
3		pw0	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$
4	3	difeq1i	$$⊢𝒫\varnothing \setminus \left\{\varnothing \right\}=\left\{\varnothing \right\}\setminus \left\{\varnothing \right\}$$
5		difid	$$⊢\left\{\varnothing \right\}\setminus \left\{\varnothing \right\}=\varnothing$$
6	4 5	eqtri	$$⊢𝒫\varnothing \setminus \left\{\varnothing \right\}=\varnothing$$
7	2 6	feq23i	$$⊢\varnothing :\mathrm{dom}\varnothing ⟶𝒫\varnothing \setminus \left\{\varnothing \right\}\leftrightarrow \varnothing :\varnothing ⟶\varnothing$$
8	1 7	mpbir	$$⊢\varnothing :\mathrm{dom}\varnothing ⟶𝒫\varnothing \setminus \left\{\varnothing \right\}$$
9		0ex	$$⊢\varnothing \in \mathrm{V}$$
10		vtxval0	$$⊢\mathrm{Vtx}\left(\varnothing \right)=\varnothing$$
11	10	eqcomi	$$⊢\varnothing =\mathrm{Vtx}\left(\varnothing \right)$$
12		iedgval0	$$⊢\mathrm{iEdg}\left(\varnothing \right)=\varnothing$$
13	12	eqcomi	$$⊢\varnothing =\mathrm{iEdg}\left(\varnothing \right)$$
14	11 13	isuhgr	$$⊢\varnothing \in \mathrm{V}\to \left(\varnothing \in \mathrm{UHGraph}\leftrightarrow \varnothing :\mathrm{dom}\varnothing ⟶𝒫\varnothing \setminus \left\{\varnothing \right\}\right)$$
15	9 14	ax-mp	$$⊢\varnothing \in \mathrm{UHGraph}\leftrightarrow \varnothing :\mathrm{dom}\varnothing ⟶𝒫\varnothing \setminus \left\{\varnothing \right\}$$
16	8 15	mpbir	$$⊢\varnothing \in \mathrm{UHGraph}$$