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