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