Theorem sltsleft

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	sltsleft	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		fvexd	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ∈ V )
2		snex	⊢ { 𝐴 } ∈ V
3	2	a1i	⊢ ( 𝐴 ∈ No → { 𝐴 } ∈ V )
4		leftf	⊢ L : No ⟶ 𝒫 No
5	4	ffvelcdmi	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ∈ 𝒫 No )
6	5	elpwid	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ No )
7		snssi	⊢ ( 𝐴 ∈ No → { 𝐴 } ⊆ No )
8		velsn	⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
9		leftval	⊢ ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 }
10	9	a1i	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } )
11	10	eleq2d	⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ) )
12		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝑥 <s 𝐴 ) )
13	11 12	bitrdi	⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝑥 <s 𝐴 ) ) )
14	13	simplbda	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ 𝐴 ) ) → 𝑥 <s 𝐴 )
15		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐴 ) )
16	14 15	imbitrrid	⊢ ( 𝑦 = 𝐴 → ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ 𝐴 ) ) → 𝑥 <s 𝑦 ) )
17	16	expd	⊢ ( 𝑦 = 𝐴 → ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) → 𝑥 <s 𝑦 ) ) )
18	8 17	sylbi	⊢ ( 𝑦 ∈ { 𝐴 } → ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) → 𝑥 <s 𝑦 ) ) )
19	18	3imp231	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ 𝐴 ) ∧ 𝑦 ∈ { 𝐴 } ) → 𝑥 <s 𝑦 )
20	1 3 6 7 19	sltsd	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } )