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 USGraph | v Vtx g VtxDeg g v = 0 V

Proof

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