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

Proof

Step Hyp Ref Expression
1 leftf ⊢ L : No ⟶ 𝒫 No
2 1 ffvelrni ⊢ A ∈ No → L ⁡ A ∈ 𝒫 No
3 2 elpwid ⊢ A ∈ No → L ⁡ A ⊆ No
4 snssi ⊢ A ∈ No → A ⊆ No
5 leftval ⊢ A ∈ No → L ⁡ A = y ∈ Old ⁡ bday ⁡ A | y < s A
6 5 eleq2d ⊢ A ∈ No → x ∈ L ⁡ A ↔ x ∈ y ∈ Old ⁡ bday ⁡ A | y < s A
7 breq1 ⊢ y = x → y < s A ↔ x < s A
8 7 elrab ⊢ x ∈ y ∈ Old ⁡ bday ⁡ A | y < s A ↔ x ∈ Old ⁡ bday ⁡ A ∧ x < s A
9 8 simprbi ⊢ x ∈ y ∈ Old ⁡ bday ⁡ A | y < s A → x < s A
10 6 9 syl6bi ⊢ A ∈ No → x ∈ L ⁡ A → x < s A
11 10 ralrimiv ⊢ A ∈ No → ∀ x ∈ L ⁡ A x < s A
12 breq2 ⊢ y = A → x < s y ↔ x < s A
13 12 ralsng ⊢ A ∈ No → ∀ y ∈ A x < s y ↔ x < s A
14 13 ralbidv ⊢ A ∈ No → ∀ x ∈ L ⁡ A ∀ y ∈ A x < s y ↔ ∀ x ∈ L ⁡ A x < s A
15 11 14 mpbird ⊢ A ∈ No → ∀ x ∈ L ⁡ A ∀ y ∈ A x < s y
16 fvex ⊢ L ⁡ A ∈ V
17 snex ⊢ A ∈ V
18 16 17 pm3.2i ⊢ L ⁡ A ∈ V ∧ A ∈ V
19 brsslt ⊢ L ⁡ A ≪ s A ↔ L ⁡ A ∈ V ∧ A ∈ V ∧ L ⁡ A ⊆ No ∧ A ⊆ No ∧ ∀ x ∈ L ⁡ A ∀ y ∈ A x < s y
20 18 19 mpbiran ⊢ L ⁡ A ≪ s A ↔ L ⁡ A ⊆ No ∧ A ⊆ No ∧ ∀ x ∈ L ⁡ A ∀ y ∈ A x < s y
21 3 4 15 20 syl3anbrc ⊢ A ∈ No → L ⁡ A ≪ s A