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 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		prssi	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → { 𝐵 , 𝐶 } ⊆ 𝐴 )
2	1	3adant1	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → { 𝐵 , 𝐶 } ⊆ 𝐴 )
3		ordelon	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ On )
4	3	3adant3	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ On )
5		ordelon	⊢ ( ( Ord 𝐴 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ On )
6		ordunpr	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∪ 𝐶 ) ∈ { 𝐵 , 𝐶 } )
7	4 5 6	3imp3i2an	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ∪ 𝐶 ) ∈ { 𝐵 , 𝐶 } )
8	2 7	sseldd	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 )