Theorem ssorduni 7780

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.)

Assertion

Ref	Expression
ssorduni	⊢ (𝐴 ⊆ On → Ord ∪ 𝐴)

Proof of Theorem ssorduni

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluni2 4878	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
2		ssel 3932	. . . . . . . . 9 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On))
3		onelss 6407	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦))
4	2, 3	syl6 36	. . . . . . . 8 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)))
5		anc2r 564	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)) → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴))))
6	4, 5	syl 18	. . . . . . 7 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴))))
7		ssuni 4900	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ⊆ ∪ 𝐴)
8	6, 7	syl8 77	. . . . . 6 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴)))
9	8	rexlimdv 3166	. . . . 5 ⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴))
10	1, 9	biimtrid 245	. . . 4 ⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴 → 𝑥 ⊆ ∪ 𝐴))
11	10	ralrimiv 3158	. . 3 ⊢ (𝐴 ⊆ On → ∀𝑥 ∈ ∪ 𝐴𝑥 ⊆ ∪ 𝐴)
12		dftr3 5225	. . 3 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑥 ∈ ∪ 𝐴𝑥 ⊆ ∪ 𝐴)
13	11, 12	sylibr 237	. 2 ⊢ (𝐴 ⊆ On → Tr ∪ 𝐴)
14		onelon 6389	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)
15	14	ex 418	. . . . . 6 ⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ∈ On))
16	2, 15	syl6 36	. . . . 5 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ∈ On)))
17	16	rexlimdv 3166	. . . 4 ⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ∈ On))
18	1, 17	biimtrid 245	. . 3 ⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ On))
19	18	ssrdv 3944	. 2 ⊢ (𝐴 ⊆ On → ∪ 𝐴 ⊆ On)
20		ordon 7778	. . 3 ⊢ Ord On
21		trssord 6381	. . . 4 ⊢ ((Tr ∪ 𝐴 ∧ ∪ 𝐴 ⊆ On ∧ Ord On) → Ord ∪ 𝐴)
22	21	3exp 1137	. . 3 ⊢ (Tr ∪ 𝐴 → (∪ 𝐴 ⊆ On → (Ord On → Ord ∪ 𝐴)))
23	20, 22	mpii 47	. 2 ⊢ (Tr ∪ 𝐴 → (∪ 𝐴 ⊆ On → Ord ∪ 𝐴))
24	13, 19, 23	sylc 66	1 ⊢ (𝐴 ⊆ On → Ord ∪ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091   ⊆ wss 3906  ∪ cuni 4874  Tr wtr 5220  Ord word 6363  Oncon0 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368

This theorem is used by:  ssonuni  7781  ssonprc  7788  orduni  7790  onsucuni  7826  limuni3  7850  onfununi  8330  tfrlem8  8373  cofon1  8660  cofon2  8661  naddcllem  8664  onssnum  10036  unialeph  10097  cfslbn  10262  hsmexlem1  10421  inaprc  10832  bdayimaon  27886  noetasuplem4  27929  noetainflem4  27933  noeta2  27983  etaslts2  28016  cutbdaybnd2lim  28019  onsupneqmaxlim0  43984  onsupnmax  43988  onsupsucismax  44039  onsucunifi  44130