Theorem noprc

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

	Ref	Expression
Assertion	noprc	⊢ ¬ No ∈ V

Proof

Step	Hyp	Ref	Expression
1		onprc	⊢ ¬ On ∈ V
2		bdayfo	⊢ bday : No –onto→ On
3		fornex	⊢ ( No ∈ V → ( bday : No –onto→ On → On ∈ V ) )
4	2 3	mpi	⊢ ( No ∈ V → On ∈ V )
5	1 4	mto	⊢ ¬ No ∈ V