Theorem noprc

Description: The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	noprc	$$⊢\neg \mathrm{No}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		onprc	$$⊢\neg \mathrm{On}\in \mathrm{V}$$
2		bdayfo	$$⊢\mathrm{bday}:\mathrm{No}\underset{onto}{⟶}\mathrm{On}$$
3		focdmex	$$⊢\mathrm{No}\in \mathrm{V}\to \left(\mathrm{bday}:\mathrm{No}\underset{onto}{⟶}\mathrm{On}\to \mathrm{On}\in \mathrm{V}\right)$$
4	2 3	mpi	$$⊢\mathrm{No}\in \mathrm{V}\to \mathrm{On}\in \mathrm{V}$$
5	1 4	mto	$$⊢\neg \mathrm{No}\in \mathrm{V}$$