Metamath Proof Explorer

Theorem ssltright

Description: A surreal is less than its right options. Theorem 0(i) of Conway p. 16. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion ssltright ⊢ A ∈ No → A ≪ s R ⁡ A

Proof

Step Hyp Ref Expression
1 snex ⊢ A ∈ V
2 1 a1i ⊢ A ∈ No → A ∈ V
3 fvexd ⊢ A ∈ No → R ⁡ A ∈ V
4 snssi ⊢ A ∈ No → A ⊆ No
5 rightf ⊢ R : No ⟶ 𝒫 No
6 5 ffvelrni ⊢ A ∈ No → R ⁡ A ∈ 𝒫 No
7 6 elpwid ⊢ A ∈ No → R ⁡ A ⊆ No
8 velsn ⊢ x ∈ A ↔ x = A
9 rightval ⊢ R ⁡ A = y ∈ Old ⁡ bday ⁡ A | A < s y
10 9 a1i ⊢ A ∈ No → R ⁡ A = y ∈ Old ⁡ bday ⁡ A | A < s y
11 10 eleq2d ⊢ A ∈ No → y ∈ R ⁡ A ↔ y ∈ y ∈ Old ⁡ bday ⁡ A | A < s y
12 rabid ⊢ y ∈ y ∈ Old ⁡ bday ⁡ A | A < s y ↔ y ∈ Old ⁡ bday ⁡ A ∧ A < s y
13 11 12 bitrdi ⊢ A ∈ No → y ∈ R ⁡ A ↔ y ∈ Old ⁡ bday ⁡ A ∧ A < s y
14 13 simplbda ⊢ A ∈ No ∧ y ∈ R ⁡ A → A < s y
15 breq1 ⊢ x = A → x < s y ↔ A < s y
16 14 15 syl5ibr ⊢ x = A → A ∈ No ∧ y ∈ R ⁡ A → x < s y
17 16 expd ⊢ x = A → A ∈ No → y ∈ R ⁡ A → x < s y
18 8 17 sylbi ⊢ x ∈ A → A ∈ No → y ∈ R ⁡ A → x < s y
19 18 3imp21 ⊢ A ∈ No ∧ x ∈ A ∧ y ∈ R ⁡ A → x < s y
20 2 3 4 7 19 ssltd ⊢ A ∈ No → A ≪ s R ⁡ A