Theorem noxp1o

Description: The Cartesian product of an ordinal and { 1o } is a surreal. (Contributed by Scott Fenton, 12-Jun-2011)

	Ref	Expression
Assertion	noxp1o	⊢ ( 𝐴 ∈ On → ( 𝐴 × { 1o } ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		1oex	⊢ 1o ∈ V
2	1	prid1	⊢ 1o ∈ { 1o , 2o }
3	2	fconst6	⊢ ( 𝐴 × { 1o } ) : 𝐴 ⟶ { 1o , 2o }
4	1	snnz	⊢ { 1o } ≠ ∅
5		dmxp	⊢ ( { 1o } ≠ ∅ → dom ( 𝐴 × { 1o } ) = 𝐴 )
6	4 5	ax-mp	⊢ dom ( 𝐴 × { 1o } ) = 𝐴
7	6	feq2i	⊢ ( ( 𝐴 × { 1o } ) : dom ( 𝐴 × { 1o } ) ⟶ { 1o , 2o } ↔ ( 𝐴 × { 1o } ) : 𝐴 ⟶ { 1o , 2o } )
8	3 7	mpbir	⊢ ( 𝐴 × { 1o } ) : dom ( 𝐴 × { 1o } ) ⟶ { 1o , 2o }
9	8	a1i	⊢ ( 𝐴 ∈ On → ( 𝐴 × { 1o } ) : dom ( 𝐴 × { 1o } ) ⟶ { 1o , 2o } )
10	6	eleq1i	⊢ ( dom ( 𝐴 × { 1o } ) ∈ On ↔ 𝐴 ∈ On )
11	10	biimpri	⊢ ( 𝐴 ∈ On → dom ( 𝐴 × { 1o } ) ∈ On )
12		elno3	⊢ ( ( 𝐴 × { 1o } ) ∈ No ↔ ( ( 𝐴 × { 1o } ) : dom ( 𝐴 × { 1o } ) ⟶ { 1o , 2o } ∧ dom ( 𝐴 × { 1o } ) ∈ On ) )
13	9 11 12	sylanbrc	⊢ ( 𝐴 ∈ On → ( 𝐴 × { 1o } ) ∈ No )