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

Metamath Proof Explorer

Theorem onun2

Description: The union of two ordinals is an ordinal. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Assertion onun2 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ On )

Proof

Step Hyp Ref Expression
1 ssequn1 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 )
2 eleq1a ⊢ ( 𝐵 ∈ On → ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → ( 𝐴 ∪ 𝐵 ) ∈ On ) )
3 2 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → ( 𝐴 ∪ 𝐵 ) ∈ On ) )
4 1 3 biimtrid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐵 ) ∈ On ) )
5 ssequn2 ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐴 )
6 eleq1a ⊢ ( 𝐴 ∈ On → ( ( 𝐴 ∪ 𝐵 ) = 𝐴 → ( 𝐴 ∪ 𝐵 ) ∈ On ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐴 → ( 𝐴 ∪ 𝐵 ) ∈ On ) )
8 5 7 biimtrid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝐴 → ( 𝐴 ∪ 𝐵 ) ∈ On ) )
9 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
10 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
11 ordtri2or2 ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
12 9 10 11 syl2an ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
13 4 8 12 mpjaod ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ On )