Description: The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | zssno | ⊢ ℤs ⊆ No |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imassrn | ⊢ ( -s “ ( ℕs × ℕs ) ) ⊆ ran -s | |
| 2 | df-zs | ⊢ ℤs = ( -s “ ( ℕs × ℕs ) ) | |
| 3 | subsfo | ⊢ -s : ( No × No ) –onto→ No | |
| 4 | forn | ⊢ ( -s : ( No × No ) –onto→ No → ran -s = No ) | |
| 5 | 3 4 | ax-mp | ⊢ ran -s = No |
| 6 | 5 | eqcomi | ⊢ No = ran -s |
| 7 | 1 2 6 | 3sstr4i | ⊢ ℤs ⊆ No |