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 e. { 1o , 2o }
Assertion noextendseq 
|- ( ( A e. No /\ B e. On ) -> ( A u. ( ( B \ dom A ) X. { X } ) ) e. No )

Proof

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