This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onun2i

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

Ref Expression
Hypotheses on.1 ⊢ A ∈ On
on.2 ⊢ B ∈ On
Assertion onun2i ⊢ A ∪ B ∈ On

Proof

Step Hyp Ref Expression
1 on.1 ⊢ A ∈ On
2 on.2 ⊢ B ∈ On
3 onun2 ⊢ A ∈ On ∧ B ∈ On → A ∪ B ∈ On
4 1 2 3 mp2an ⊢ A ∪ B ∈ On