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

Proof

Step	Hyp	Ref	Expression
1		leftf	⊢ L : No ⟶ 𝒫 No
2	1	ffvelrni	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ∈ 𝒫 No )
3	2	elpwid	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ No )
4		snssi	⊢ ( 𝐴 ∈ No → { 𝐴 } ⊆ No )
5		leftval	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) = { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑦 <s 𝐴 } )
6	5	eleq2d	⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) ↔ 𝑥 ∈ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑦 <s 𝐴 } ) )
7		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 <s 𝐴 ↔ 𝑥 <s 𝐴 ) )
8	7	elrab	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑦 <s 𝐴 } ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝑥 <s 𝐴 ) )
9	8	simprbi	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑦 <s 𝐴 } → 𝑥 <s 𝐴 )
10	6 9	syl6bi	⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) → 𝑥 <s 𝐴 ) )
11	10	ralrimiv	⊢ ( 𝐴 ∈ No → ∀ 𝑥 ∈ ( L ‘ 𝐴 ) 𝑥 <s 𝐴 )
12		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐴 ) )
13	12	ralsng	⊢ ( 𝐴 ∈ No → ( ∀ 𝑦 ∈ { 𝐴 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐴 ) )
14	13	ralbidv	⊢ ( 𝐴 ∈ No → ( ∀ 𝑥 ∈ ( L ‘ 𝐴 ) ∀ 𝑦 ∈ { 𝐴 } 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ ( L ‘ 𝐴 ) 𝑥 <s 𝐴 ) )
15	11 14	mpbird	⊢ ( 𝐴 ∈ No → ∀ 𝑥 ∈ ( L ‘ 𝐴 ) ∀ 𝑦 ∈ { 𝐴 } 𝑥 <s 𝑦 )
16		fvex	⊢ ( L ‘ 𝐴 ) ∈ V
17		snex	⊢ { 𝐴 } ∈ V
18	16 17	pm3.2i	⊢ ( ( L ‘ 𝐴 ) ∈ V ∧ { 𝐴 } ∈ V )
19		brsslt	⊢ ( ( L ‘ 𝐴 ) <<s { 𝐴 } ↔ ( ( ( L ‘ 𝐴 ) ∈ V ∧ { 𝐴 } ∈ V ) ∧ ( ( L ‘ 𝐴 ) ⊆ No ∧ { 𝐴 } ⊆ No ∧ ∀ 𝑥 ∈ ( L ‘ 𝐴 ) ∀ 𝑦 ∈ { 𝐴 } 𝑥 <s 𝑦 ) ) )
20	18 19	mpbiran	⊢ ( ( L ‘ 𝐴 ) <<s { 𝐴 } ↔ ( ( L ‘ 𝐴 ) ⊆ No ∧ { 𝐴 } ⊆ No ∧ ∀ 𝑥 ∈ ( L ‘ 𝐴 ) ∀ 𝑦 ∈ { 𝐴 } 𝑥 <s 𝑦 ) )
21	3 4 15 20	syl3anbrc	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } )