Theorem uhgr0

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

	Ref	Expression
Assertion	uhgr0	|- (/) e. UHGraph

Proof

Step	Hyp	Ref	Expression
1		f0	|- (/) : (/) --> (/)
2		dm0	|- dom (/) = (/)
3		pw0	|- ~P (/) = { (/) }
4	3	difeq1i	|- ( ~P (/) \ { (/) } ) = ( { (/) } \ { (/) } )
5		difid	|- ( { (/) } \ { (/) } ) = (/)
6	4 5	eqtri	|- ( ~P (/) \ { (/) } ) = (/)
7	2 6	feq23i	|- ( (/) : dom (/) --> ( ~P (/) \ { (/) } ) <-> (/) : (/) --> (/) )
8	1 7	mpbir	|- (/) : dom (/) --> ( ~P (/) \ { (/) } )
9		0ex	|- (/) e. _V
10		vtxval0	|- ( Vtx ` (/) ) = (/)
11	10	eqcomi	|- (/) = ( Vtx ` (/) )
12		iedgval0	|- ( iEdg ` (/) ) = (/)
13	12	eqcomi	|- (/) = ( iEdg ` (/) )
14	11 13	isuhgr	|- ( (/) e. _V -> ( (/) e. UHGraph <-> (/) : dom (/) --> ( ~P (/) \ { (/) } ) ) )
15	9 14	ax-mp	|- ( (/) e. UHGraph <-> (/) : dom (/) --> ( ~P (/) \ { (/) } ) )
16	8 15	mpbir	|- (/) e. UHGraph