Theorem griedg0prc

Description: The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Hypothesis	griedg0prc.u	$$⊢U=\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}$$
Assertion	griedg0prc	$$⊢U\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		griedg0prc.u	$$⊢U=\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		feq1	$$⊢e=\varnothing \to \left(e:\varnothing ⟶\varnothing \leftrightarrow \varnothing :\varnothing ⟶\varnothing \right)$$
4		f0	$$⊢\varnothing :\varnothing ⟶\varnothing$$
5	2 3 4	ceqsexv2d	$$⊢\exists ee:\varnothing ⟶\varnothing$$
6		opabn1stprc	$$⊢\exists ee:\varnothing ⟶\varnothing \to \left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}$$
7	5 6	ax-mp	$$⊢\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}$$
8		neleq1	$$⊢U=\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\to \left(U\notin \mathrm{V}\leftrightarrow \left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}\right)$$
9	1 8	ax-mp	$$⊢U\notin \mathrm{V}\leftrightarrow \left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}$$
10	7 9	mpbir	$$⊢U\notin \mathrm{V}$$