Theorem ordunmax

Description: The union of two ordinals is equal to their maximum. (Contributed by BTernaryTau, 7-Oct-2026)

	Ref	Expression
Assertion	ordunmax	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∪ 𝐵 ) = if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtri2or2	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
2	1	ord	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ⊆ 𝐵 → 𝐵 ⊆ 𝐴 ) )
3		ssequn2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐴 )
4	2 3	imbitrdi	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐵 ) = 𝐴 ) )
5		iffalse	⊢ ( ¬ 𝐴 ⊆ 𝐵 → if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) = 𝐴 )
6	4 5	jca2	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ⊆ 𝐵 → ( ( 𝐴 ∪ 𝐵 ) = 𝐴 ∧ if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) = 𝐴 ) ) )
7		eqtr3	⊢ ( ( ( 𝐴 ∪ 𝐵 ) = 𝐴 ∧ if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) = 𝐴 ) → ( 𝐴 ∪ 𝐵 ) = if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) )
8	6 7	syl6	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐵 ) = if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) ) )
9		ssequn1	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 )
10	9	biimpi	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐵 ) = 𝐵 )
11		iftrue	⊢ ( 𝐴 ⊆ 𝐵 → if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
12	10 11	eqtr4d	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐵 ) = if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) )
13	8 12	pm2.61d2	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∪ 𝐵 ) = if ( 𝐴 ⊆ 𝐵 , 𝐵 , 𝐴 ) )