Metamath Proof Explorer

Theorem rgrusgrprc

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

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

Proof

Step Hyp Ref Expression
1 elopab 
 |-  ( p e. { <. v , e >. | e : (/) --> (/) } <-> E. v E. e ( p = <. v , e >. /\ e : (/) --> (/) ) )
2 f0bi 
 |-  ( e : (/) --> (/) <-> e = (/) )
3 opeq2 
 |-  ( e = (/) -> <. v , e >. = <. v , (/) >. )
4 usgr0eop 
 |-  ( v e. _V -> <. v , (/) >. e. USGraph )
5 4 elv 
 |-  <. v , (/) >. e. USGraph
6 3 5 eqeltrdi 
 |-  ( e = (/) -> <. v , e >. e. USGraph )
7 vex 
 |-  v e. _V
8 vex 
 |-  e e. _V
9 7 8 opiedgfvi 
 |-  ( iEdg ` <. v , e >. ) = e
10 id 
 |-  ( e = (/) -> e = (/) )
11 9 10 syl5eq 
 |-  ( e = (/) -> ( iEdg ` <. v , e >. ) = (/) )
12 6 11 jca 
 |-  ( e = (/) -> ( <. v , e >. e. USGraph /\ ( iEdg ` <. v , e >. ) = (/) ) )
13 2 12 sylbi 
 |-  ( e : (/) --> (/) -> ( <. v , e >. e. USGraph /\ ( iEdg ` <. v , e >. ) = (/) ) )
14 13 adantl 
 |-  ( ( p = <. v , e >. /\ e : (/) --> (/) ) -> ( <. v , e >. e. USGraph /\ ( iEdg ` <. v , e >. ) = (/) ) )
15 eleq1 
 |-  ( p = <. v , e >. -> ( p e. USGraph <-> <. v , e >. e. USGraph ) )
16 fveqeq2 
 |-  ( p = <. v , e >. -> ( ( iEdg ` p ) = (/) <-> ( iEdg ` <. v , e >. ) = (/) ) )
17 15 16 anbi12d 
 |-  ( p = <. v , e >. -> ( ( p e. USGraph /\ ( iEdg ` p ) = (/) ) <-> ( <. v , e >. e. USGraph /\ ( iEdg ` <. v , e >. ) = (/) ) ) )
18 17 adantr 
 |-  ( ( p = <. v , e >. /\ e : (/) --> (/) ) -> ( ( p e. USGraph /\ ( iEdg ` p ) = (/) ) <-> ( <. v , e >. e. USGraph /\ ( iEdg ` <. v , e >. ) = (/) ) ) )
19 14 18 mpbird 
 |-  ( ( p = <. v , e >. /\ e : (/) --> (/) ) -> ( p e. USGraph /\ ( iEdg ` p ) = (/) ) )
20 fveqeq2 
 |-  ( g = p -> ( ( iEdg ` g ) = (/) <-> ( iEdg ` p ) = (/) ) )
21 20 elrab 
 |-  ( p e. { g e. USGraph | ( iEdg ` g ) = (/) } <-> ( p e. USGraph /\ ( iEdg ` p ) = (/) ) )
22 19 21 sylibr 
 |-  ( ( p = <. v , e >. /\ e : (/) --> (/) ) -> p e. { g e. USGraph | ( iEdg ` g ) = (/) } )
23 22 exlimivv 
 |-  ( E. v E. e ( p = <. v , e >. /\ e : (/) --> (/) ) -> p e. { g e. USGraph | ( iEdg ` g ) = (/) } )
24 1 23 sylbi 
 |-  ( p e. { <. v , e >. | e : (/) --> (/) } -> p e. { g e. USGraph | ( iEdg ` g ) = (/) } )
25 24 ssriv 
 |-  { <. v , e >. | e : (/) --> (/) } C_ { g e. USGraph | ( iEdg ` g ) = (/) }
26 eqid 
 |-  { <. v , e >. | e : (/) --> (/) } = { <. v , e >. | e : (/) --> (/) }
27 26 griedg0prc 
 |-  { <. v , e >. | e : (/) --> (/) } e/ _V
28 prcssprc 
 |-  ( ( { <. v , e >. | e : (/) --> (/) } C_ { g e. USGraph | ( iEdg ` g ) = (/) } /\ { <. v , e >. | e : (/) --> (/) } e/ _V ) -> { g e. USGraph | ( iEdg ` g ) = (/) } e/ _V )
29 25 27 28 mp2an 
 |-  { g e. USGraph | ( iEdg ` g ) = (/) } e/ _V
30 df-3an 
 |-  ( ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) <-> ( ( g e. USGraph /\ 0 e. NN0* ) /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) )
31 30 bicomi 
 |-  ( ( ( g e. USGraph /\ 0 e. NN0* ) /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) <-> ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) )
32 31 a1i 
 |-  ( g e. USGraph -> ( ( ( g e. USGraph /\ 0 e. NN0* ) /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) <-> ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) ) )
33 0xnn0 
 |-  0 e. NN0*
34 ibar 
 |-  ( ( g e. USGraph /\ 0 e. NN0* ) -> ( A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 <-> ( ( g e. USGraph /\ 0 e. NN0* ) /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) ) )
35 33 34 mpan2 
 |-  ( g e. USGraph -> ( A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 <-> ( ( g e. USGraph /\ 0 e. NN0* ) /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) ) )
36 eqid 
 |-  ( Vtx ` g ) = ( Vtx ` g )
37 eqid 
 |-  ( VtxDeg ` g ) = ( VtxDeg ` g )
38 36 37 isrusgr0 
 |-  ( ( g e. USGraph /\ 0 e. NN0* ) -> ( g RegUSGraph 0 <-> ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) ) )
39 33 38 mpan2 
 |-  ( g e. USGraph -> ( g RegUSGraph 0 <-> ( g e. USGraph /\ 0 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) ) )
40 32 35 39 3bitr4d 
 |-  ( g e. USGraph -> ( A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 <-> g RegUSGraph 0 ) )
41 40 rabbiia 
 |-  { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } = { g e. USGraph | g RegUSGraph 0 }
42 usgr0edg0rusgr 
 |-  ( g e. USGraph -> ( g RegUSGraph 0 <-> ( Edg ` g ) = (/) ) )
43 usgruhgr 
 |-  ( g e. USGraph -> g e. UHGraph )
44 uhgriedg0edg0 
 |-  ( g e. UHGraph -> ( ( Edg ` g ) = (/) <-> ( iEdg ` g ) = (/) ) )
45 43 44 syl 
 |-  ( g e. USGraph -> ( ( Edg ` g ) = (/) <-> ( iEdg ` g ) = (/) ) )
46 42 45 bitrd 
 |-  ( g e. USGraph -> ( g RegUSGraph 0 <-> ( iEdg ` g ) = (/) ) )
47 46 rabbiia 
 |-  { g e. USGraph | g RegUSGraph 0 } = { g e. USGraph | ( iEdg ` g ) = (/) }
48 41 47 eqtri 
 |-  { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } = { g e. USGraph | ( iEdg ` g ) = (/) }
49 neleq1 
 |-  ( { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } = { g e. USGraph | ( iEdg ` g ) = (/) } -> ( { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V <-> { g e. USGraph | ( iEdg ` g ) = (/) } e/ _V ) )
50 48 49 ax-mp 
 |-  ( { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V <-> { g e. USGraph | ( iEdg ` g ) = (/) } e/ _V )
51 29 50 mpbir 
 |-  { g e. USGraph | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V