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 { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V

Proof

Step Hyp Ref Expression
1 elopab ( 𝑝 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ↔ ∃ 𝑣𝑒 ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) )
2 f0bi ( 𝑒 : ∅ ⟶ ∅ ↔ 𝑒 = ∅ )
3 opeq2 ( 𝑒 = ∅ → ⟨ 𝑣 , 𝑒 ⟩ = ⟨ 𝑣 , ∅ ⟩ )
4 usgr0eop ( 𝑣 ∈ V → ⟨ 𝑣 , ∅ ⟩ ∈ USGraph )
5 4 elv 𝑣 , ∅ ⟩ ∈ USGraph
6 3 5 eqeltrdi ( 𝑒 = ∅ → ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph )
7 vex 𝑣 ∈ V
8 vex 𝑒 ∈ V
9 7 8 opiedgfvi ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = 𝑒
10 id ( 𝑒 = ∅ → 𝑒 = ∅ )
11 9 10 syl5eq ( 𝑒 = ∅ → ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ )
12 6 11 jca ( 𝑒 = ∅ → ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ ) )
13 2 12 sylbi ( 𝑒 : ∅ ⟶ ∅ → ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ ) )
14 13 adantl ( ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ ) )
15 eleq1 ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ → ( 𝑝 ∈ USGraph ↔ ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ) )
16 fveqeq2 ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ → ( ( iEdg ‘ 𝑝 ) = ∅ ↔ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ ) )
17 15 16 anbi12d ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ → ( ( 𝑝 ∈ USGraph ∧ ( iEdg ‘ 𝑝 ) = ∅ ) ↔ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ ) ) )
18 17 adantr ( ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → ( ( 𝑝 ∈ USGraph ∧ ( iEdg ‘ 𝑝 ) = ∅ ) ↔ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ ) ) )
19 14 18 mpbird ( ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → ( 𝑝 ∈ USGraph ∧ ( iEdg ‘ 𝑝 ) = ∅ ) )
20 fveqeq2 ( 𝑔 = 𝑝 → ( ( iEdg ‘ 𝑔 ) = ∅ ↔ ( iEdg ‘ 𝑝 ) = ∅ ) )
21 20 elrab ( 𝑝 ∈ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } ↔ ( 𝑝 ∈ USGraph ∧ ( iEdg ‘ 𝑝 ) = ∅ ) )
22 19 21 sylibr ( ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → 𝑝 ∈ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } )
23 22 exlimivv ( ∃ 𝑣𝑒 ( 𝑝 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → 𝑝 ∈ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } )
24 1 23 sylbi ( 𝑝 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } → 𝑝 ∈ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } )
25 24 ssriv { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ⊆ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ }
26 eqid { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ }
27 26 griedg0prc { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V
28 prcssprc ( ( { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ⊆ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } ∧ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V ) → { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } ∉ V )
29 25 27 28 mp2an { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } ∉ V
30 df-3an ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ↔ ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
31 30 bicomi ( ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ↔ ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
32 31 a1i ( 𝑔 ∈ USGraph → ( ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ↔ ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ) )
33 0xnn0 0 ∈ ℕ0*
34 ibar ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ↔ ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ) )
35 33 34 mpan2 ( 𝑔 ∈ USGraph → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ↔ ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ) )
36 eqid ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 )
37 eqid ( VtxDeg ‘ 𝑔 ) = ( VtxDeg ‘ 𝑔 )
38 36 37 isrusgr0 ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ) → ( 𝑔 RegUSGraph 0 ↔ ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ) )
39 33 38 mpan2 ( 𝑔 ∈ USGraph → ( 𝑔 RegUSGraph 0 ↔ ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ) )
40 32 35 39 3bitr4d ( 𝑔 ∈ USGraph → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ↔ 𝑔 RegUSGraph 0 ) )
41 40 rabbiia { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } = { 𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0 }
42 usgr0edg0rusgr ( 𝑔 ∈ USGraph → ( 𝑔 RegUSGraph 0 ↔ ( Edg ‘ 𝑔 ) = ∅ ) )
43 usgruhgr ( 𝑔 ∈ USGraph → 𝑔 ∈ UHGraph )
44 uhgriedg0edg0 ( 𝑔 ∈ UHGraph → ( ( Edg ‘ 𝑔 ) = ∅ ↔ ( iEdg ‘ 𝑔 ) = ∅ ) )
45 43 44 syl ( 𝑔 ∈ USGraph → ( ( Edg ‘ 𝑔 ) = ∅ ↔ ( iEdg ‘ 𝑔 ) = ∅ ) )
46 42 45 bitrd ( 𝑔 ∈ USGraph → ( 𝑔 RegUSGraph 0 ↔ ( iEdg ‘ 𝑔 ) = ∅ ) )
47 46 rabbiia { 𝑔 ∈ USGraph ∣ 𝑔 RegUSGraph 0 } = { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ }
48 41 47 eqtri { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } = { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ }
49 neleq1 ( { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } = { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } → ( { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V ↔ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } ∉ V ) )
50 48 49 ax-mp ( { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V ↔ { 𝑔 ∈ USGraph ∣ ( iEdg ‘ 𝑔 ) = ∅ } ∉ V )
51 29 50 mpbir { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V