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 ⊢ 𝑋 ∈ { 1o , 2o }
Assertion noextendseq ( ( 𝐴 ∈ No ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ ( ( 𝐵 ∖ dom 𝐴 ) × { 𝑋 } ) ) ∈ No )

Proof

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