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

Metamath Proof Explorer

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 ) → ( 𝐵 ∪ 𝐶 ) ∈ { 𝐵 , 𝐶 } )