Theorem madessno

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

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

Proof

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