Theorem uhgr0e

Description: The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

	Ref	Expression
Hypotheses	uhgr0e.g	|- ( ph -> G e. W )
	uhgr0e.e	|- ( ph -> ( iEdg ` G ) = (/) )
Assertion	uhgr0e	|- ( ph -> G e. UHGraph )

Proof

Step	Hyp	Ref	Expression
1		uhgr0e.g	|- ( ph -> G e. W )
2		uhgr0e.e	|- ( ph -> ( iEdg ` G ) = (/) )
3		f0	|- (/) : (/) --> ( ~P ( Vtx ` G ) \ { (/) } )
4		dm0	|- dom (/) = (/)
5	4	feq2i	|- ( (/) : dom (/) --> ( ~P ( Vtx ` G ) \ { (/) } ) <-> (/) : (/) --> ( ~P ( Vtx ` G ) \ { (/) } ) )
6	3 5	mpbir	|- (/) : dom (/) --> ( ~P ( Vtx ` G ) \ { (/) } )
7		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
8		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
9	7 8	isuhgr	|- ( G e. W -> ( G e. UHGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
10	1 9	syl	|- ( ph -> ( G e. UHGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
11		id	|- ( ( iEdg ` G ) = (/) -> ( iEdg ` G ) = (/) )
12		dmeq	|- ( ( iEdg ` G ) = (/) -> dom ( iEdg ` G ) = dom (/) )
13	11 12	feq12d	|- ( ( iEdg ` G ) = (/) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) <-> (/) : dom (/) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
14	2 13	syl	|- ( ph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) <-> (/) : dom (/) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
15	10 14	bitrd	|- ( ph -> ( G e. UHGraph <-> (/) : dom (/) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
16	6 15	mpbiri	|- ( ph -> G e. UHGraph )