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

Theorem ordsson 7154
Description: Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
ordsson (Ord 𝐴𝐴 ⊆ On)

Proof of Theorem ordsson
StepHypRef Expression
1 ordon 7147 . 2 Ord On
2 ordeleqon 7153 . . . . 5 (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
32biimpi 206 . . . 4 (Ord 𝐴 → (𝐴 ∈ On ∨ 𝐴 = On))
43adantr 472 . . 3 ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
5 ordsseleq 5913 . . 3 ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
64, 5mpbird 247 . 2 ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
71, 6mpan2 709 1 (Ord 𝐴𝐴 ⊆ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383   = wceq 1632  wcel 2139  wss 3715  Ord word 5883  Oncon0 5884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-tr 4905  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-ord 5887  df-on 5888
This theorem is referenced by:  onss  7155  orduni  7159  ordsucuniel  7189  ordsucuni  7194  iordsmo  7623  dfrecs3  7638  tfr2b  7661  tz7.44-2  7672  ordiso2  8585  ordtypelem7  8594  ordtypelem8  8595  oiid  8611  r1tr  8812  r1ordg  8814  r1ord3g  8815  r1pwss  8820  r1val1  8822  rankwflemb  8829  r1elwf  8832  rankr1ai  8834  cflim2  9277  cfss  9279  cfslb  9280  cfslbn  9281  cfslb2n  9282  cofsmo  9283  coftr  9287  inaprc  9850  dford5  31915  rdgprc  32005  nosepon  32124  limsucncmpi  32750
  Copyright terms: Public domain W3C validator