Metamath Proof Explorer

Theorem rgrprcx

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

Ref Expression
Assertion rgrprcx 
|- { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V

Proof

Step Hyp Ref Expression
1 rgrprc 
 |-  { g | g RegGraph 0 } e/ _V
2 0xnn0 
 |-  0 e. NN0*
3 vex 
 |-  g e. _V
4 eqid 
 |-  ( Vtx ` g ) = ( Vtx ` g )
5 eqid 
 |-  ( VtxDeg ` g ) = ( VtxDeg ` g )
6 4 5 isrgr 
 |-  ( ( g e. _V /\ 0 e. NN0* ) -> ( g RegGraph 0 <-> ( 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) ) )
7 3 2 6 mp2an 
 |-  ( g RegGraph 0 <-> ( 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) )
8 2 7 mpbiran 
 |-  ( g RegGraph 0 <-> A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 )
9 8 bicomi 
 |-  ( A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 <-> g RegGraph 0 )
10 9 abbii 
 |-  { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } = { g | g RegGraph 0 }
11 neleq1 
 |-  ( { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } = { g | g RegGraph 0 } -> ( { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V <-> { g | g RegGraph 0 } e/ _V ) )
12 10 11 ax-mp 
 |-  ( { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V <-> { g | g RegGraph 0 } e/ _V )
13 1 12 mpbir 
 |-  { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V