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

Metamath Proof Explorer

Theorem ordequn

Description: The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of TakeutiZaring p. 40. (Contributed by NM, 28-Nov-2003)

		Ref	Expression
	Assertion	ordequn	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtri2or2	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) )
2	1	orcomd	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐶 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐶 ) )
3		ssequn2	⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐵 )
4		eqeq1	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝐴 = 𝐵 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐵 ) )
5	3 4	bitr4id	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝐶 ⊆ 𝐵 ↔ 𝐴 = 𝐵 ) )
6		ssequn1	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐶 )
7		eqeq1	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝐴 = 𝐶 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐶 ) )
8	6 7	bitr4id	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝐵 ⊆ 𝐶 ↔ 𝐴 = 𝐶 ) )
9	5 8	orbi12d	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( ( 𝐶 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
10	2 9	syl5ibcom	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 = ( 𝐵 ∪ 𝐶 ) → ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )