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	|- ( A e. On -> ( A X. { 1o } ) e. No )

Proof

Step	Hyp	Ref	Expression
1		1oex	|- 1o e. _V
2	1	prid1	|- 1o e. { 1o , 2o }
3	2	fconst6	|- ( A X. { 1o } ) : A --> { 1o , 2o }
4	1	snnz	|- { 1o } =/= (/)
5		dmxp	|- ( { 1o } =/= (/) -> dom ( A X. { 1o } ) = A )
6	4 5	ax-mp	|- dom ( A X. { 1o } ) = A
7	6	feq2i	|- ( ( A X. { 1o } ) : dom ( A X. { 1o } ) --> { 1o , 2o } <-> ( A X. { 1o } ) : A --> { 1o , 2o } )
8	3 7	mpbir	|- ( A X. { 1o } ) : dom ( A X. { 1o } ) --> { 1o , 2o }
9	8	a1i	|- ( A e. On -> ( A X. { 1o } ) : dom ( A X. { 1o } ) --> { 1o , 2o } )
10	6	eleq1i	|- ( dom ( A X. { 1o } ) e. On <-> A e. On )
11	10	biimpri	|- ( A e. On -> dom ( A X. { 1o } ) e. On )
12		elno3	|- ( ( A X. { 1o } ) e. No <-> ( ( A X. { 1o } ) : dom ( A X. { 1o } ) --> { 1o , 2o } /\ dom ( A X. { 1o } ) e. On ) )
13	9 11 12	sylanbrc	|- ( A e. On -> ( A X. { 1o } ) e. No )