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 eqtrid ⊢ ( 𝑒 = ∅ → ( 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