Metamath Proof Explorer


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 fvexd ( 𝐴 No → ( L ‘ 𝐴 ) ∈ V )
2 snex { 𝐴 } ∈ V
3 2 a1i ( 𝐴 No → { 𝐴 } ∈ V )
4 leftf L : No ⟶ 𝒫 No
5 4 ffvelrni ( 𝐴 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 syl5ibr ( 𝑦 = 𝐴 → ( ( 𝐴 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 ssltd ( 𝐴 No → ( L ‘ 𝐴 ) <<s { 𝐴 } )