Metamath Proof Explorer

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 ⊢ A ∈ No → L ⁡ A ≪ s A

Proof

Step Hyp Ref Expression
1 fvexd ⊢ A ∈ No → L ⁡ A ∈ V
2 snex ⊢ A ∈ V
3 2 a1i ⊢ A ∈ No → A ∈ V
4 leftf ⊢ L : No ⟶ 𝒫 No
5 4 ffvelcdmi ⊢ A ∈ No → L ⁡ A ∈ 𝒫 No
6 5 elpwid ⊢ A ∈ No → L ⁡ A ⊆ No
7 snssi ⊢ A ∈ No → A ⊆ No
8 velsn ⊢ y ∈ A ↔ y = A
9 leftval ⊢ L ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A
10 9 a1i ⊢ A ∈ No → L ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A
11 10 eleq2d ⊢ A ∈ No → x ∈ L ⁡ A ↔ x ∈ x ∈ Old ⁡ bday ⁡ A | x < s A
12 rabid ⊢ x ∈ x ∈ Old ⁡ bday ⁡ A | x < s A ↔ x ∈ Old ⁡ bday ⁡ A ∧ x < s A
13 11 12 bitrdi ⊢ A ∈ No → x ∈ L ⁡ A ↔ x ∈ Old ⁡ bday ⁡ A ∧ x < s A
14 13 simplbda ⊢ A ∈ No ∧ x ∈ L ⁡ A → x < s A
15 breq2 ⊢ y = A → x < s y ↔ x < s A
16 14 15 imbitrrid ⊢ y = A → A ∈ No ∧ x ∈ L ⁡ A → x < s y
17 16 expd ⊢ y = A → A ∈ No → x ∈ L ⁡ A → x < s y
18 8 17 sylbi ⊢ y ∈ A → A ∈ No → x ∈ L ⁡ A → x < s y
19 18 3imp231 ⊢ A ∈ No ∧ x ∈ L ⁡ A ∧ y ∈ A → x < s y
20 1 3 6 7 19 sltsd ⊢ A ∈ No → L ⁡ A ≪ s A