Metamath Proof Explorer


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 AOnA×1𝑜No

Proof

Step Hyp Ref Expression
1 1oex 1𝑜V
2 1 prid1 1𝑜1𝑜2𝑜
3 2 fconst6 A×1𝑜:A1𝑜2𝑜
4 1 snnz 1𝑜
5 dmxp 1𝑜domA×1𝑜=A
6 4 5 ax-mp domA×1𝑜=A
7 6 feq2i A×1𝑜:domA×1𝑜1𝑜2𝑜A×1𝑜:A1𝑜2𝑜
8 3 7 mpbir A×1𝑜:domA×1𝑜1𝑜2𝑜
9 8 a1i AOnA×1𝑜:domA×1𝑜1𝑜2𝑜
10 6 eleq1i domA×1𝑜OnAOn
11 10 biimpri AOndomA×1𝑜On
12 elno3 A×1𝑜NoA×1𝑜:domA×1𝑜1𝑜2𝑜domA×1𝑜On
13 9 11 12 sylanbrc AOnA×1𝑜No