Theorem onun2i

Description: The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994)

	Ref	Expression
Hypotheses	on.1	⊢ 𝐴 ∈ On
	on.2	⊢ 𝐵 ∈ On
Assertion	onun2i	⊢ ( 𝐴 ∪ 𝐵 ) ∈ On

Proof

Step	Hyp	Ref	Expression
1		on.1	⊢ 𝐴 ∈ On
2		on.2	⊢ 𝐵 ∈ On
3	2	onordi	⊢ Ord 𝐵
4	1	onordi	⊢ Ord 𝐴
5		ordtri2or	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ⊆ 𝐵 ) )
6	3 4 5	mp2an	⊢ ( 𝐵 ∈ 𝐴 ∨ 𝐴 ⊆ 𝐵 )
7	1	oneluni	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐴 ∪ 𝐵 ) = 𝐴 )
8	7 1	syl6eqel	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐴 ∪ 𝐵 ) ∈ On )
9		ssequn1	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 )
10		eleq1	⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → ( ( 𝐴 ∪ 𝐵 ) ∈ On ↔ 𝐵 ∈ On ) )
11	2 10	mpbiri	⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → ( 𝐴 ∪ 𝐵 ) ∈ On )
12	9 11	sylbi	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐵 ) ∈ On )
13	8 12	jaoi	⊢ ( ( 𝐵 ∈ 𝐴 ∨ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ∈ On )
14	6 13	ax-mp	⊢ ( 𝐴 ∪ 𝐵 ) ∈ On