Metamath Proof Explorer


Theorem ordsucun

Description: The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordsucun Ord A Ord B suc A B = suc A suc B

Proof

Step Hyp Ref Expression
1 ordun Ord A Ord B Ord A B
2 ordsuc Ord A B Ord suc A B
3 ordelon Ord suc A B x suc A B x On
4 3 ex Ord suc A B x suc A B x On
5 2 4 sylbi Ord A B x suc A B x On
6 1 5 syl Ord A Ord B x suc A B x On
7 ordsuc Ord A Ord suc A
8 ordsuc Ord B Ord suc B
9 ordun Ord suc A Ord suc B Ord suc A suc B
10 ordelon Ord suc A suc B x suc A suc B x On
11 10 ex Ord suc A suc B x suc A suc B x On
12 9 11 syl Ord suc A Ord suc B x suc A suc B x On
13 7 8 12 syl2anb Ord A Ord B x suc A suc B x On
14 ordssun Ord A Ord B x A B x A x B
15 14 adantl x On Ord A Ord B x A B x A x B
16 ordsssuc x On Ord A B x A B x suc A B
17 1 16 sylan2 x On Ord A Ord B x A B x suc A B
18 ordsssuc x On Ord A x A x suc A
19 18 adantrr x On Ord A Ord B x A x suc A
20 ordsssuc x On Ord B x B x suc B
21 20 adantrl x On Ord A Ord B x B x suc B
22 19 21 orbi12d x On Ord A Ord B x A x B x suc A x suc B
23 15 17 22 3bitr3d x On Ord A Ord B x suc A B x suc A x suc B
24 elun x suc A suc B x suc A x suc B
25 23 24 bitr4di x On Ord A Ord B x suc A B x suc A suc B
26 25 expcom Ord A Ord B x On x suc A B x suc A suc B
27 6 13 26 pm5.21ndd Ord A Ord B x suc A B x suc A suc B
28 27 eqrdv Ord A Ord B suc A B = suc A suc B