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

Theorem ssorduni 7224
Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (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.
StepHypRef Expression
1 eluni2 4645 . . . . 5 (𝑥 𝐴 ↔ ∃𝑦𝐴 𝑥𝑦)
2 ssel 3803 . . . . . . . . 9 (𝐴 ⊆ On → (𝑦𝐴𝑦 ∈ On))
3 onelss 5991 . . . . . . . . 9 (𝑦 ∈ On → (𝑥𝑦𝑥𝑦))
42, 3syl6 35 . . . . . . . 8 (𝐴 ⊆ On → (𝑦𝐴 → (𝑥𝑦𝑥𝑦)))
5 anc2r 546 . . . . . . . 8 ((𝑦𝐴 → (𝑥𝑦𝑥𝑦)) → (𝑦𝐴 → (𝑥𝑦 → (𝑥𝑦𝑦𝐴))))
64, 5syl 17 . . . . . . 7 (𝐴 ⊆ On → (𝑦𝐴 → (𝑥𝑦 → (𝑥𝑦𝑦𝐴))))
7 ssuni 4665 . . . . . . 7 ((𝑥𝑦𝑦𝐴) → 𝑥 𝐴)
86, 7syl8 76 . . . . . 6 (𝐴 ⊆ On → (𝑦𝐴 → (𝑥𝑦𝑥 𝐴)))
98rexlimdv 3229 . . . . 5 (𝐴 ⊆ On → (∃𝑦𝐴 𝑥𝑦𝑥 𝐴))
101, 9syl5bi 233 . . . 4 (𝐴 ⊆ On → (𝑥 𝐴𝑥 𝐴))
1110ralrimiv 3164 . . 3 (𝐴 ⊆ On → ∀𝑥 𝐴𝑥 𝐴)
12 dftr3 4961 . . 3 (Tr 𝐴 ↔ ∀𝑥 𝐴𝑥 𝐴)
1311, 12sylibr 225 . 2 (𝐴 ⊆ On → Tr 𝐴)
14 onelon 5974 . . . . . . 7 ((𝑦 ∈ On ∧ 𝑥𝑦) → 𝑥 ∈ On)
1514ex 399 . . . . . 6 (𝑦 ∈ On → (𝑥𝑦𝑥 ∈ On))
162, 15syl6 35 . . . . 5 (𝐴 ⊆ On → (𝑦𝐴 → (𝑥𝑦𝑥 ∈ On)))
1716rexlimdv 3229 . . . 4 (𝐴 ⊆ On → (∃𝑦𝐴 𝑥𝑦𝑥 ∈ On))
181, 17syl5bi 233 . . 3 (𝐴 ⊆ On → (𝑥 𝐴𝑥 ∈ On))
1918ssrdv 3815 . 2 (𝐴 ⊆ On → 𝐴 ⊆ On)
20 ordon 7221 . . 3 Ord On
21 trssord 5966 . . . 4 ((Tr 𝐴 𝐴 ⊆ On ∧ Ord On) → Ord 𝐴)
22213exp 1141 . . 3 (Tr 𝐴 → ( 𝐴 ⊆ On → (Ord On → Ord 𝐴)))
2320, 22mpii 46 . 2 (Tr 𝐴 → ( 𝐴 ⊆ On → Ord 𝐴))
2413, 19, 23sylc 65 1 (𝐴 ⊆ On → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2157  wral 3107  wrex 3108  wss 3780   cuni 4641  Tr wtr 4957  Ord word 5948  Oncon0 5949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109  ax-un 7188
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-tr 4958  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-ord 5952  df-on 5953
This theorem is referenced by:  ssonuni  7225  ssonprc  7231  orduni  7233  onsucuni  7267  limuni3  7291  onfununi  7683  tfrlem8  7725  onssnum  9155  unialeph  9216  cfslbn  9383  hsmexlem1  9542  inaprc  9952  bdayimaon  32185  nosupbday  32193  noetalem3  32207  noetalem4  32208
  Copyright terms: Public domain W3C validator