Theorem ssorduni 7720

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 4864	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
2		ssel 3924	. . . . . . . . 9 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On))
3		onelss 6355	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦))
4	2, 3	syl6 35	. . . . . . . 8 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)))
5		anc2r 554	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)) → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴))))
6	4, 5	syl 17	. . . . . . 7 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴))))
7		ssuni 4885	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ⊆ ∪ 𝐴)
8	6, 7	syl8 76	. . . . . 6 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴)))
9	8	rexlimdv 3132	. . . . 5 ⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴))
10	1, 9	biimtrid 242	. . . 4 ⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴 → 𝑥 ⊆ ∪ 𝐴))
11	10	ralrimiv 3124	. . 3 ⊢ (𝐴 ⊆ On → ∀𝑥 ∈ ∪ 𝐴𝑥 ⊆ ∪ 𝐴)
12		dftr3 5207	. . 3 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑥 ∈ ∪ 𝐴𝑥 ⊆ ∪ 𝐴)
13	11, 12	sylibr 234	. 2 ⊢ (𝐴 ⊆ On → Tr ∪ 𝐴)
14		onelon 6338	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)
15	14	ex 412	. . . . . 6 ⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ∈ On))
16	2, 15	syl6 35	. . . . 5 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ∈ On)))
17	16	rexlimdv 3132	. . . 4 ⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ∈ On))
18	1, 17	biimtrid 242	. . 3 ⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ On))
19	18	ssrdv 3936	. 2 ⊢ (𝐴 ⊆ On → ∪ 𝐴 ⊆ On)
20		ordon 7718	. . 3 ⊢ Ord On
21		trssord 6330	. . . 4 ⊢ ((Tr ∪ 𝐴 ∧ ∪ 𝐴 ⊆ On ∧ Ord On) → Ord ∪ 𝐴)
22	21	3exp 1119	. . 3 ⊢ (Tr ∪ 𝐴 → (∪ 𝐴 ⊆ On → (Ord On → Ord ∪ 𝐴)))
23	20, 22	mpii 46	. 2 ⊢ (Tr ∪ 𝐴 → (∪ 𝐴 ⊆ On → Ord ∪ 𝐴))
24	13, 19, 23	sylc 65	1 ⊢ (𝐴 ⊆ On → Ord ∪ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057   ⊆ wss 3898  ∪ cuni 4860  Tr wtr 5202  Ord word 6312  Oncon0 6313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6316  df-on 6317

This theorem is referenced by:  ssonuni  7721  ssonprc  7728  orduni  7730  onsucuni  7766  limuni3  7790  onfununi  8269  tfrlem8  8311  cofon1  8595  cofon2  8596  naddcllem  8599  onssnum  9940  unialeph  10001  cfslbn  10167  hsmexlem1  10326  inaprc  10736  bdayimaon  27635  noetasuplem4  27678  noetainflem4  27682  noeta2  27727  etasslt2  27758  scutbdaybnd2lim  27761  onsupneqmaxlim0  43344  onsupnmax  43348  onsupsucismax  43399  onsucunifi  43490