onun2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > onun2		Structured version Visualization version GIF version

Theorem onun2 6473

Description: The union of two ordinals is an ordinal. (Contributed by Scott Fenton, 9-Aug-2024.)

**Assertion**
Ref	Expression
onun2	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On)

**Proof of Theorem onun2**
Step	Hyp	Ref	Expression
1		ssequn1 4184	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		eleq1a 2855	. . . 4 ⊢ (𝐵 ∈ On → ((𝐴 ∪ 𝐵) = 𝐵 → (𝐴 ∪ 𝐵) ∈ On))
3	2	adantl 487	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∪ 𝐵) = 𝐵 → (𝐴 ∪ 𝐵) ∈ On))
4	1, 3	biimtrid 245	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐵) ∈ On))
5		ssequn2 4187	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐴 ∪ 𝐵) = 𝐴)
6		eleq1a 2855	. . . 4 ⊢ (𝐴 ∈ On → ((𝐴 ∪ 𝐵) = 𝐴 → (𝐴 ∪ 𝐵) ∈ On))
7	6	adantr 486	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∪ 𝐵) = 𝐴 → (𝐴 ∪ 𝐵) ∈ On))
8	5, 7	biimtrid 245	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝐴 → (𝐴 ∪ 𝐵) ∈ On))
9		eloni 6372	. . 3 ⊢ (𝐴 ∈ On → Ord 𝐴)
10		eloni 6372	. . 3 ⊢ (𝐵 ∈ On → Ord 𝐵)
11		ordtri2or2 6464	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
12	9, 10, 11	syl2an 608	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
13	4, 8, 12	mpjaod 874	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ⊆ wss 3895 ∪ cun 4149 Ord word 6361 Oncon0 6362

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-sep 5248 ax-pr 5390

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-tr 5212 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-ord 6365 df-on 6366

This theorem is used by: onun2i 6486 nosupinfsep 28094 r0maxss 35942 maxssj0 35945 j0ltalephlem 35946 j0ltaleph 35947 onexlimgt 44338 omabs2 44427 onsucunitp 44468