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 syl6bi
 |-  ( ( 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 ) = (/) ) )