Metamath Proof Explorer

Theorem rusgrprc

Description: The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020)

Ref Expression
Assertion rusgrprc 
|- { g | g RegUSGraph 0 } e/ _V

Proof

Step Hyp Ref Expression
1 rgrusgrprc 
 |-  { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V
2 vex 
 |-  g e. _V
3 0xnn0 
 |-  0 e. NN0*
4 eqid 
 |-  ( Vtx ` g ) = ( Vtx ` g )
5 eqid 
 |-  ( VtxDeg ` g ) = ( VtxDeg ` g )
6 4 5 isrusgr0 
 |-  ( ( g e. _V /\ 0 e. NN0* ) -> ( g RegUSGraph 0 <-> ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) ) )
7 2 3 6 mp2an 
 |-  ( g RegUSGraph 0 <-> ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) )
8 3ancomb 
 |-  ( ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) <-> ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 /\ 0 e. NN0* ) )
9 df-3an 
 |-  ( ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 /\ 0 e. NN0* ) <-> ( ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) /\ 0 e. NN0* ) )
10 3 9 mpbiran2 
 |-  ( ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 /\ 0 e. NN0* ) <-> ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) )
11 7 8 10 3bitri 
 |-  ( g RegUSGraph 0 <-> ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) )
12 11 abbii 
 |-  { g | g RegUSGraph 0 } = { g | ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) }
13 df-rab 
 |-  { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } = { g | ( g e. USGraph /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) }
14 12 13 eqtr4i 
 |-  { g | g RegUSGraph 0 } = { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 }
15 neleq1 
 |-  ( { g | g RegUSGraph 0 } = { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } -> ( { g | g RegUSGraph 0 } e/ _V <-> { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V ) )
16 14 15 ax-mp 
 |-  ( { g | g RegUSGraph 0 } e/ _V <-> { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V )
17 1 16 mpbir 
 |-  { g | g RegUSGraph 0 } e/ _V