This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )