![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssorduni | Structured version Visualization version GIF version |
Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. Lemma 2.7 of [Schloeder] p. 4. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Ref | Expression |
---|---|
ssorduni | ⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluni2 4874 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) | |
2 | ssel 3942 | . . . . . . . . 9 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On)) | |
3 | onelss 6364 | . . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)) | |
4 | 2, 3 | syl6 35 | . . . . . . . 8 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦))) |
5 | anc2r 556 | . . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)) → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴)))) | |
6 | 4, 5 | syl 17 | . . . . . . 7 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴)))) |
7 | ssuni 4898 | . . . . . . 7 ⊢ ((𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ⊆ ∪ 𝐴) | |
8 | 6, 7 | syl8 76 | . . . . . 6 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴))) |
9 | 8 | rexlimdv 3151 | . . . . 5 ⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴)) |
10 | 1, 9 | biimtrid 241 | . . . 4 ⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴 → 𝑥 ⊆ ∪ 𝐴)) |
11 | 10 | ralrimiv 3143 | . . 3 ⊢ (𝐴 ⊆ On → ∀𝑥 ∈ ∪ 𝐴𝑥 ⊆ ∪ 𝐴) |
12 | dftr3 5233 | . . 3 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑥 ∈ ∪ 𝐴𝑥 ⊆ ∪ 𝐴) | |
13 | 11, 12 | sylibr 233 | . 2 ⊢ (𝐴 ⊆ On → Tr ∪ 𝐴) |
14 | onelon 6347 | . . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On) | |
15 | 14 | ex 414 | . . . . . 6 ⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ∈ On)) |
16 | 2, 15 | syl6 35 | . . . . 5 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ∈ On))) |
17 | 16 | rexlimdv 3151 | . . . 4 ⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ∈ On)) |
18 | 1, 17 | biimtrid 241 | . . 3 ⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ On)) |
19 | 18 | ssrdv 3955 | . 2 ⊢ (𝐴 ⊆ On → ∪ 𝐴 ⊆ On) |
20 | ordon 7716 | . . 3 ⊢ Ord On | |
21 | trssord 6339 | . . . 4 ⊢ ((Tr ∪ 𝐴 ∧ ∪ 𝐴 ⊆ On ∧ Ord On) → Ord ∪ 𝐴) | |
22 | 21 | 3exp 1120 | . . 3 ⊢ (Tr ∪ 𝐴 → (∪ 𝐴 ⊆ On → (Ord On → Ord ∪ 𝐴))) |
23 | 20, 22 | mpii 46 | . 2 ⊢ (Tr ∪ 𝐴 → (∪ 𝐴 ⊆ On → Ord ∪ 𝐴)) |
24 | 13, 19, 23 | sylc 65 | 1 ⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3065 ∃wrex 3074 ⊆ wss 3915 ∪ cuni 4870 Tr wtr 5227 Ord word 6321 Oncon0 6322 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-pss 3934 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-tr 5228 df-eprel 5542 df-po 5550 df-so 5551 df-fr 5593 df-we 5595 df-ord 6325 df-on 6326 |
This theorem is referenced by: ssonuni 7719 ssonprc 7727 orduni 7729 onsucuni 7768 limuni3 7793 onfununi 8292 tfrlem8 8335 cofon1 8623 cofon2 8624 naddcllem 8627 onssnum 9983 unialeph 10044 cfslbn 10210 hsmexlem1 10369 inaprc 10779 bdayimaon 27057 noetasuplem4 27100 noetainflem4 27104 noeta2 27146 etasslt2 27175 scutbdaybnd2lim 27178 onsupneqmaxlim0 41587 onsupnmax 41591 onsupsucismax 41643 onsucunifi 41715 |
Copyright terms: Public domain | W3C validator |