Theorem ordunpr

Description: The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Assertion	ordunpr	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∪ 𝐶 ) ∈ { 𝐵 , 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
2		eloni	⊢ ( 𝐶 ∈ On → Ord 𝐶 )
3		ordtri2or2	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) )
5	4	orcomd	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐶 ) )
6		ssequn2	⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐵 )
7		ssequn1	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐶 )
8	6 7	orbi12i	⊢ ( ( 𝐶 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐶 ) ↔ ( ( 𝐵 ∪ 𝐶 ) = 𝐵 ∨ ( 𝐵 ∪ 𝐶 ) = 𝐶 ) )
9	5 8	sylib	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐵 ∪ 𝐶 ) = 𝐵 ∨ ( 𝐵 ∪ 𝐶 ) = 𝐶 ) )
10		unexg	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
11		elprg	⊢ ( ( 𝐵 ∪ 𝐶 ) ∈ V → ( ( 𝐵 ∪ 𝐶 ) ∈ { 𝐵 , 𝐶 } ↔ ( ( 𝐵 ∪ 𝐶 ) = 𝐵 ∨ ( 𝐵 ∪ 𝐶 ) = 𝐶 ) ) )
12	10 11	syl	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐵 ∪ 𝐶 ) ∈ { 𝐵 , 𝐶 } ↔ ( ( 𝐵 ∪ 𝐶 ) = 𝐵 ∨ ( 𝐵 ∪ 𝐶 ) = 𝐶 ) ) )
13	9 12	mpbird	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∪ 𝐶 ) ∈ { 𝐵 , 𝐶 } )