Theorem rightirr

Description: No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	rightirr	Could not format assertion : No typesetting found for |- -. X e. ( _Right ` X ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oldirr	$$⊢\neg X\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
2		rightssold	Could not format ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) : No typesetting found for |- ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) with typecode |-
3	2	sseli	Could not format ( X e. ( _Right ` X ) -> X e. ( _Old ` ( bday ` X ) ) ) : No typesetting found for |- ( X e. ( _Right ` X ) -> X e. ( _Old ` ( bday ` X ) ) ) with typecode |-
4	1 3	mto	Could not format -. X e. ( _Right ` X ) : No typesetting found for |- -. X e. ( _Right ` X ) with typecode |-