Metamath Proof Explorer

Theorem uhgr0vb

Description: The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 9-Oct-2020)

Ref Expression
Assertion uhgr0vb 
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 uhgrf 
 |-  ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) )
4 pweq 
 |-  ( ( Vtx ` G ) = (/) -> ~P ( Vtx ` G ) = ~P (/) )
5 4 difeq1d 
 |-  ( ( Vtx ` G ) = (/) -> ( ~P ( Vtx ` G ) \ { (/) } ) = ( ~P (/) \ { (/) } ) )
6 pw0 
 |-  ~P (/) = { (/) }
7 6 difeq1i 
 |-  ( ~P (/) \ { (/) } ) = ( { (/) } \ { (/) } )
8 difid 
 |-  ( { (/) } \ { (/) } ) = (/)
9 7 8 eqtri 
 |-  ( ~P (/) \ { (/) } ) = (/)
10 5 9 eqtrdi 
 |-  ( ( Vtx ` G ) = (/) -> ( ~P ( Vtx ` G ) \ { (/) } ) = (/) )
11 10 adantl 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ~P ( Vtx ` G ) \ { (/) } ) = (/) )
12 11 feq3d 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) ) )
13 f00 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) <-> ( ( iEdg ` G ) = (/) /\ dom ( iEdg ` G ) = (/) ) )
14 13 simplbi 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) -> ( iEdg ` G ) = (/) )
15 12 14 biimtrdi 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) -> ( iEdg ` G ) = (/) ) )
16 3 15 syl5 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph -> ( iEdg ` G ) = (/) ) )
17 simpl 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. W )
18 simpr 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
19 17 18 uhgr0e 
 |-  ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. UHGraph )
20 19 ex 
 |-  ( G e. W -> ( ( iEdg ` G ) = (/) -> G e. UHGraph ) )
21 20 adantr 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) = (/) -> G e. UHGraph ) )
22 16 21 impbid 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) )