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 → B C ⊆ A
2 1 3adant1 ⊢ Ord ⁡ A ∧ B ∈ A ∧ C ∈ A → B C ⊆ 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 ∈ B C
7 4 5 6 3imp3i2an ⊢ Ord ⁡ A ∧ B ∈ A ∧ C ∈ A → B ∪ C ∈ B C
8 2 7 sseldd ⊢ Ord ⁡ A ∧ B ∈ A ∧ C ∈ A → B ∪ C ∈ A