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