Metamath Proof Explorer

Theorem ordunel

Description: The maximum of two ordinals belongs to a third if each of them do. (Contributed by NM, 18-Sep-2006) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion ordunel ⊢Ord⁡A∧B∈A∧C∈A→B∪C∈A

Proof

Step Hyp Ref Expression
1 prssi ⊢B∈A∧C∈A→BC⊆A
2 1 3adant1 ⊢Ord⁡A∧B∈A∧C∈A→BC⊆A
3 ordelon ⊢Ord⁡A∧B∈A→B∈On
4 3 3adant3 ⊢Ord⁡A∧B∈A∧C∈A→B∈On
5 ordelon ⊢Ord⁡A∧C∈A→C∈On
6 ordunpr ⊢B∈On∧C∈On→B∪C∈BC
7 4 5 6 3imp3i2an ⊢Ord⁡A∧B∈A∧C∈A→B∪C∈BC
8 2 7 sseldd ⊢Ord⁡A∧B∈A∧C∈A→B∪C∈A