Metamath Proof Explorer

Theorem cplgr0

Description: The null graph (with no vertices and no edges) represented by the empty set is a complete graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion cplgr0 
|- (/) e. ComplGraph

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. v e. (/) v e. ( UnivVtx ` (/) )
2 vtxval0 
 |-  ( Vtx ` (/) ) = (/)
3 2 raleqi 
 |-  ( A. v e. ( Vtx ` (/) ) v e. ( UnivVtx ` (/) ) <-> A. v e. (/) v e. ( UnivVtx ` (/) ) )
4 1 3 mpbir 
 |-  A. v e. ( Vtx ` (/) ) v e. ( UnivVtx ` (/) )
5 0ex 
 |-  (/) e. _V
6 eqid 
 |-  ( Vtx ` (/) ) = ( Vtx ` (/) )
7 6 iscplgr 
 |-  ( (/) e. _V -> ( (/) e. ComplGraph <-> A. v e. ( Vtx ` (/) ) v e. ( UnivVtx ` (/) ) ) )
8 5 7 ax-mp 
 |-  ( (/) e. ComplGraph <-> A. v e. ( Vtx ` (/) ) v e. ( UnivVtx ` (/) ) )
9 4 8 mpbir 
 |-  (/) e. ComplGraph