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

Metamath Proof Explorer

Theorem ordun

Description: The maximum (i.e., union) of two ordinals is ordinal. Exercise 12 of TakeutiZaring p. 40. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordun ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
2 ordequn ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∪ 𝐵 ) = 𝐵 ) ) )
3 1 2 mpi ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∪ 𝐵 ) = 𝐵 ) )
4 ordeq ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐴 → ( Ord ( 𝐴 ∪ 𝐵 ) ↔ Ord 𝐴 ) )
5 4 biimprcd ⊢ ( Ord 𝐴 → ( ( 𝐴 ∪ 𝐵 ) = 𝐴 → Ord ( 𝐴 ∪ 𝐵 ) ) )
6 ordeq ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → ( Ord ( 𝐴 ∪ 𝐵 ) ↔ Ord 𝐵 ) )
7 6 biimprcd ⊢ ( Ord 𝐵 → ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → Ord ( 𝐴 ∪ 𝐵 ) ) )
8 5 7 jaao ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( ( 𝐴 ∪ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∪ 𝐵 ) = 𝐵 ) → Ord ( 𝐴 ∪ 𝐵 ) ) )
9 3 8 mpd ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord ( 𝐴 ∪ 𝐵 ) )