Theorem onno

Description: Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023)

	Ref	Expression
Assertion	onno	⊢ ( 𝐴 ∈ On → ( 𝐴 × { 2o } ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		2oex	⊢ 2o ∈ V
2	1	prid2	⊢ 2o ∈ { 1o , 2o }
3		onnog	⊢ ( ( 𝐴 ∈ On ∧ 2o ∈ { 1o , 2o } ) → ( 𝐴 × { 2o } ) ∈ No )
4	2 3	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 × { 2o } ) ∈ No )