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