Theorem rusgrprc

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

	Ref	Expression
Assertion	rusgrprc	⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		rgrusgrprc	⊢ { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V
2		vex	⊢ 𝑔 ∈ V
3		0xnn0	⊢ 0 ∈ ℕ0*
4		eqid	⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 )
5		eqid	⊢ ( VtxDeg ‘ 𝑔 ) = ( VtxDeg ‘ 𝑔 )
6	4 5	isrusgr0	⊢ ( ( 𝑔 ∈ V ∧ 0 ∈ ℕ0* ) → ( 𝑔 RegUSGraph 0 ↔ ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ) )
7	2 3 6	mp2an	⊢ ( 𝑔 RegUSGraph 0 ↔ ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
8		3ancomb	⊢ ( ( 𝑔 ∈ USGraph ∧ 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ↔ ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ∧ 0 ∈ ℕ0* ) )
9		df-3an	⊢ ( ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ∧ 0 ∈ ℕ0* ) ↔ ( ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ∧ 0 ∈ ℕ0* ) )
10	3 9	mpbiran2	⊢ ( ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ∧ 0 ∈ ℕ0* ) ↔ ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
11	7 8 10	3bitri	⊢ ( 𝑔 RegUSGraph 0 ↔ ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
12	11	abbii	⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } = { 𝑔 ∣ ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) }
13		df-rab	⊢ { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } = { 𝑔 ∣ ( 𝑔 ∈ USGraph ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) }
14	12 13	eqtr4i	⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } = { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 }
15		neleq1	⊢ ( { 𝑔 ∣ 𝑔 RegUSGraph 0 } = { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } → ( { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V ↔ { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V ) )
16	14 15	ax-mp	⊢ ( { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V ↔ { 𝑔 ∈ USGraph ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V )
17	1 16	mpbir	⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V