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 ( 𝐴 ∪ 𝐵 ) )