Metamath Proof Explorer


Theorem noextendseq

Description: Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021)

Ref Expression
Hypothesis noextend.1 X 1 𝑜 2 𝑜
Assertion noextendseq A No B On A B dom A × X No

Proof

Step Hyp Ref Expression
1 noextend.1 X 1 𝑜 2 𝑜
2 nofun A No Fun A
3 fnconstg X 1 𝑜 2 𝑜 B dom A × X Fn B dom A
4 fnfun B dom A × X Fn B dom A Fun B dom A × X
5 1 3 4 mp2b Fun B dom A × X
6 snnzg X 1 𝑜 2 𝑜 X
7 dmxp X dom B dom A × X = B dom A
8 1 6 7 mp2b dom B dom A × X = B dom A
9 8 ineq2i dom A dom B dom A × X = dom A B dom A
10 disjdif dom A B dom A =
11 9 10 eqtri dom A dom B dom A × X =
12 funun Fun A Fun B dom A × X dom A dom B dom A × X = Fun A B dom A × X
13 11 12 mpan2 Fun A Fun B dom A × X Fun A B dom A × X
14 2 5 13 sylancl A No Fun A B dom A × X
15 14 adantr A No B On Fun A B dom A × X
16 dmun dom A B dom A × X = dom A dom B dom A × X
17 8 uneq2i dom A dom B dom A × X = dom A B dom A
18 16 17 eqtri dom A B dom A × X = dom A B dom A
19 nodmon A No dom A On
20 undif dom A B dom A B dom A = B
21 eleq1a B On dom A B dom A = B dom A B dom A On
22 21 adantl dom A On B On dom A B dom A = B dom A B dom A On
23 20 22 syl5bi dom A On B On dom A B dom A B dom A On
24 ssdif0 B dom A B dom A =
25 uneq2 B dom A = dom A B dom A = dom A
26 un0 dom A = dom A
27 25 26 eqtrdi B dom A = dom A B dom A = dom A
28 27 eleq1d B dom A = dom A B dom A On dom A On
29 28 biimprcd dom A On B dom A = dom A B dom A On
30 29 adantr dom A On B On B dom A = dom A B dom A On
31 24 30 syl5bi dom A On B On B dom A dom A B dom A On
32 eloni dom A On Ord dom A
33 eloni B On Ord B
34 ordtri2or2 Ord dom A Ord B dom A B B dom A
35 32 33 34 syl2an dom A On B On dom A B B dom A
36 23 31 35 mpjaod dom A On B On dom A B dom A On
37 19 36 sylan A No B On dom A B dom A On
38 18 37 eqeltrid A No B On dom A B dom A × X On
39 rnun ran A B dom A × X = ran A ran B dom A × X
40 norn A No ran A 1 𝑜 2 𝑜
41 40 adantr A No B On ran A 1 𝑜 2 𝑜
42 rnxpss ran B dom A × X X
43 snssi X 1 𝑜 2 𝑜 X 1 𝑜 2 𝑜
44 1 43 ax-mp X 1 𝑜 2 𝑜
45 42 44 sstri ran B dom A × X 1 𝑜 2 𝑜
46 unss ran A 1 𝑜 2 𝑜 ran B dom A × X 1 𝑜 2 𝑜 ran A ran B dom A × X 1 𝑜 2 𝑜
47 41 45 46 sylanblc A No B On ran A ran B dom A × X 1 𝑜 2 𝑜
48 39 47 eqsstrid A No B On ran A B dom A × X 1 𝑜 2 𝑜
49 elno2 A B dom A × X No Fun A B dom A × X dom A B dom A × X On ran A B dom A × X 1 𝑜 2 𝑜
50 15 38 48 49 syl3anbrc A No B On A B dom A × X No