Theorem newssno

Description: New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	newssno	Could not format assertion : No typesetting found for |- ( _New ` A ) C_ No with typecode |-

Proof

Step	Hyp	Ref	Expression
1		newf	Could not format _New : On --> ~P No : No typesetting found for |- _New : On --> ~P No with typecode |-
2		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
3	1 2	f0cli	Could not format ( _New ` A ) e. ~P No : No typesetting found for |- ( _New ` A ) e. ~P No with typecode |-
4		elpwi	Could not format ( ( _New ` A ) e. ~P No -> ( _New ` A ) C_ No ) : No typesetting found for |- ( ( _New ` A ) e. ~P No -> ( _New ` A ) C_ No ) with typecode |-
5	3 4	ax-mp	Could not format ( _New ` A ) C_ No : No typesetting found for |- ( _New ` A ) C_ No with typecode |-