Theorem rgrprcx

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

	Ref	Expression
Assertion	rgrprcx	⊢ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		rgrprc	⊢ { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V
2		0xnn0	⊢ 0 ∈ ℕ0*
3		vex	⊢ 𝑔 ∈ V
4		eqid	⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 )
5		eqid	⊢ ( VtxDeg ‘ 𝑔 ) = ( VtxDeg ‘ 𝑔 )
6	4 5	isrgr	⊢ ( ( 𝑔 ∈ V ∧ 0 ∈ ℕ0* ) → ( 𝑔 RegGraph 0 ↔ ( 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) ) )
7	3 2 6	mp2an	⊢ ( 𝑔 RegGraph 0 ↔ ( 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
8	2 7	mpbiran	⊢ ( 𝑔 RegGraph 0 ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 )
9	8	bicomi	⊢ ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ↔ 𝑔 RegGraph 0 )
10	9	abbii	⊢ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } = { 𝑔 ∣ 𝑔 RegGraph 0 }
11		neleq1	⊢ ( { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } = { 𝑔 ∣ 𝑔 RegGraph 0 } → ( { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V ↔ { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V ) )
12	10 11	ax-mp	⊢ ( { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V ↔ { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V )
13	1 12	mpbir	⊢ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V