Metamath Proof Explorer


Theorem noextend

Description: Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021)

Ref Expression
Hypothesis noextend.1 X1𝑜2𝑜
Assertion noextend ANoAdomAXNo

Proof

Step Hyp Ref Expression
1 noextend.1 X1𝑜2𝑜
2 nofun ANoFunA
3 dmexg ANodomAV
4 funsng domAVX1𝑜2𝑜FundomAX
5 3 1 4 sylancl ANoFundomAX
6 1 elexi XV
7 6 dmsnop domdomAX=domA
8 7 ineq2i domAdomdomAX=domAdomA
9 nodmord ANoOrddomA
10 ordirr OrddomA¬domAdomA
11 9 10 syl ANo¬domAdomA
12 disjsn domAdomA=¬domAdomA
13 11 12 sylibr ANodomAdomA=
14 8 13 eqtrid ANodomAdomdomAX=
15 funun FunAFundomAXdomAdomdomAX=FunAdomAX
16 2 5 14 15 syl21anc ANoFunAdomAX
17 7 uneq2i domAdomdomAX=domAdomA
18 dmun domAdomAX=domAdomdomAX
19 df-suc sucdomA=domAdomA
20 17 18 19 3eqtr4i domAdomAX=sucdomA
21 nodmon ANodomAOn
22 suceloni domAOnsucdomAOn
23 21 22 syl ANosucdomAOn
24 20 23 eqeltrid ANodomAdomAXOn
25 rnun ranAdomAX=ranArandomAX
26 rnsnopg domAVrandomAX=X
27 3 26 syl ANorandomAX=X
28 27 uneq2d ANoranArandomAX=ranAX
29 25 28 eqtrid ANoranAdomAX=ranAX
30 norn ANoranA1𝑜2𝑜
31 snssi X1𝑜2𝑜X1𝑜2𝑜
32 1 31 mp1i ANoX1𝑜2𝑜
33 30 32 unssd ANoranAX1𝑜2𝑜
34 29 33 eqsstrd ANoranAdomAX1𝑜2𝑜
35 elno2 AdomAXNoFunAdomAXdomAdomAXOnranAdomAX1𝑜2𝑜
36 16 24 34 35 syl3anbrc ANoAdomAXNo