Theorem ssltright

Description: A surreal is less than its right options. Theorem 0(i) of Conway p. 16. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	ssltright	Could not format assertion : No typesetting found for |- ( A e. No -> { A } <

Proof

Step	Hyp	Ref	Expression
1		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
2	1	a1i	$$⊢A\in \mathrm{No}\to \left\{A\right\}\in \mathrm{V}$$
3		fvexd	Could not format ( A e. No -> ( _Right ` A ) e. _V ) : No typesetting found for |- ( A e. No -> ( _Right ` A ) e. _V ) with typecode |-
4		snssi	$$⊢A\in \mathrm{No}\to \left\{A\right\}\subseteq \mathrm{No}$$
5		rightf	Could not format _Right : No --> ~P No : No typesetting found for |- _Right : No --> ~P No with typecode |-
6	5	ffvelcdmi	Could not format ( A e. No -> ( _Right ` A ) e. ~P No ) : No typesetting found for |- ( A e. No -> ( _Right ` A ) e. ~P No ) with typecode |-
7	6	elpwid	Could not format ( A e. No -> ( _Right ` A ) C_ No ) : No typesetting found for |- ( A e. No -> ( _Right ` A ) C_ No ) with typecode |-
8		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
9		rightval	Could not format ( _Right ` A ) = { y e. ( _Old ` ( bday ` A ) ) | A
10	9	a1i	Could not format ( A e. No -> ( _Right ` A ) = { y e. ( _Old ` ( bday ` A ) ) | A ( _Right ` A ) = { y e. ( _Old ` ( bday ` A ) ) | A
11	10	eleq2d	Could not format ( A e. No -> ( y e. ( _Right ` A ) <-> y e. { y e. ( _Old ` ( bday ` A ) ) | A ( y e. ( _Right ` A ) <-> y e. { y e. ( _Old ` ( bday ` A ) ) | A
12		rabid	$$⊢y\in \left\{y\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)|A{<}_{s}y\right\}\leftrightarrow \left(y\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\wedge A{<}_{s}y\right)$$
13	11 12	bitrdi	Could not format ( A e. No -> ( y e. ( _Right ` A ) <-> ( y e. ( _Old ` ( bday ` A ) ) /\ A ( y e. ( _Right ` A ) <-> ( y e. ( _Old ` ( bday ` A ) ) /\ A
14	13	simplbda	Could not format ( ( A e. No /\ y e. ( _Right ` A ) ) -> A A
15		breq1	$$⊢x=A\to \left(x{<}_{s}y\leftrightarrow A{<}_{s}y\right)$$
16	14 15	imbitrrid	Could not format ( x = A -> ( ( A e. No /\ y e. ( _Right ` A ) ) -> x ( ( A e. No /\ y e. ( _Right ` A ) ) -> x
17	16	expd	Could not format ( x = A -> ( A e. No -> ( y e. ( _Right ` A ) -> x ( A e. No -> ( y e. ( _Right ` A ) -> x
18	8 17	sylbi	Could not format ( x e. { A } -> ( A e. No -> ( y e. ( _Right ` A ) -> x ( A e. No -> ( y e. ( _Right ` A ) -> x
19	18	3imp21	Could not format ( ( A e. No /\ x e. { A } /\ y e. ( _Right ` A ) ) -> x x
20	2 3 4 7 19	ssltd	Could not format ( A e. No -> { A } < { A } <