Metamath Proof Explorer

Theorem onunel

Description: The union of two ordinals is in a third iff both of the first two are. (Contributed by Scott Fenton, 10-Sep-2024)

Ref Expression
Assertion onunel ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∪ B ∈ C ↔ A ∈ C ∧ B ∈ C

Proof

Step Hyp Ref Expression
1 ssequn1 ⊢ A ⊆ B ↔ A ∪ B = B
2 1 biimpi ⊢ A ⊆ B → A ∪ B = B
3 2 eleq1d ⊢ A ⊆ B → A ∪ B ∈ C ↔ B ∈ C
4 3 adantl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ⊆ B → A ∪ B ∈ C ↔ B ∈ C
5 ontr2 ⊢ A ∈ On ∧ C ∈ On → A ⊆ B ∧ B ∈ C → A ∈ C
6 5 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ∧ B ∈ C → A ∈ C
7 6 expdimp ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ⊆ B → B ∈ C → A ∈ C
8 7 pm4.71rd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ⊆ B → B ∈ C ↔ A ∈ C ∧ B ∈ C
9 4 8 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ A ⊆ B → A ∪ B ∈ C ↔ A ∈ C ∧ B ∈ C
10 ssequn2 ⊢ B ⊆ A ↔ A ∪ B = A
11 10 biimpi ⊢ B ⊆ A → A ∪ B = A
12 11 eleq1d ⊢ B ⊆ A → A ∪ B ∈ C ↔ A ∈ C
13 12 adantl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ B ⊆ A → A ∪ B ∈ C ↔ A ∈ C
14 ontr2 ⊢ B ∈ On ∧ C ∈ On → B ⊆ A ∧ A ∈ C → B ∈ C
15 14 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ⊆ A ∧ A ∈ C → B ∈ C
16 15 expdimp ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ B ⊆ A → A ∈ C → B ∈ C
17 16 pm4.71d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ B ⊆ A → A ∈ C ↔ A ∈ C ∧ B ∈ C
18 13 17 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ B ⊆ A → A ∪ B ∈ C ↔ A ∈ C ∧ B ∈ C
19 eloni ⊢ A ∈ On → Ord ⁡ A
20 eloni ⊢ B ∈ On → Ord ⁡ B
21 ordtri2or2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ∨ B ⊆ A
22 19 20 21 syl2an ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ∨ B ⊆ A
23 22 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ∨ B ⊆ A
24 9 18 23 mpjaodan ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∪ B ∈ C ↔ A ∈ C ∧ B ∈ C