Theorem ssltleft

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

	Ref	Expression
Assertion	ssltleft	Could not format assertion : No typesetting found for |- ( A e. No -> ( _Left ` A ) <

Proof

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