Description: The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 20-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | rightssno | ⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ No ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rightssold | ⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) ) | |
2 | bdayelon | ⊢ ( bday ‘ 𝐴 ) ∈ On | |
3 | oldf | ⊢ O : On ⟶ 𝒫 No | |
4 | 3 | ffvelrni | ⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ∈ 𝒫 No ) |
5 | 4 | elpwid | ⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No ) |
6 | 2 5 | ax-mp | ⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No |
7 | 1 6 | sstrdi | ⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ No ) |