Metamath Proof Explorer

Theorem usgr0

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

Ref Expression
Assertion usgr0 
|- (/) e. USGraph

Proof

Step Hyp Ref Expression
1 f10 
 |-  (/) : (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 }
2 dm0 
 |-  dom (/) = (/)
3 f1eq2 
 |-  ( dom (/) = (/) -> ( (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } <-> (/) : (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } ) )
4 2 3 ax-mp 
 |-  ( (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } <-> (/) : (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } )
5 1 4 mpbir 
 |-  (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 }
6 0ex 
 |-  (/) e. _V
7 vtxval0 
 |-  ( Vtx ` (/) ) = (/)
8 7 eqcomi 
 |-  (/) = ( Vtx ` (/) )
9 iedgval0 
 |-  ( iEdg ` (/) ) = (/)
10 9 eqcomi 
 |-  (/) = ( iEdg ` (/) )
11 8 10 isusgr 
 |-  ( (/) e. _V -> ( (/) e. USGraph <-> (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } ) )
12 6 11 ax-mp 
 |-  ( (/) e. USGraph <-> (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } )
13 5 12 mpbir 
 |-  (/) e. USGraph