Description: The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | rgrprc | ⊢ { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rusgrrgr | ⊢ ( 𝑔 RegUSGraph 0 → 𝑔 RegGraph 0 ) | |
2 | 1 | ss2abi | ⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ⊆ { 𝑔 ∣ 𝑔 RegGraph 0 } |
3 | rusgrprc | ⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V | |
4 | prcssprc | ⊢ ( ( { 𝑔 ∣ 𝑔 RegUSGraph 0 } ⊆ { 𝑔 ∣ 𝑔 RegGraph 0 } ∧ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V ) → { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V ) | |
5 | 2 3 4 | mp2an | ⊢ { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V |