Theorem ordsson 7733

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

Step	Hyp	Ref	Expression
1		ordon 7727	. 2 ⊢ Ord On
2		ordeleqon 7732	. . . 4 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	birani 504	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
4		ordsseleq 6346	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
5	3, 4	mpbird 258	. 2 ⊢ ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
6	1, 5	mpan2 697	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ⊆ wss 3890  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5187  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321

This theorem is referenced by:  dford5  7734  onss  7735  orduni  7739  ordsuci  7758  ordsucuniel  7771  ordsucuni  7776  iordsmo  8294  dfrecs3  8309  tfr2b  8332  tz7.44-2  8343  ordiso2  9427  ordtypelem7  9436  ordtypelem8  9437  oiid  9453  r1tr  9698  r1ordg  9700  r1ord3g  9701  r1pwss  9706  r1val1  9708  rankwflemb  9715  r1elwf  9718  rankr1ai  9720  cflim2  10183  cfss  10185  cfslb  10186  cfslbn  10187  cfslb2n  10188  cofsmo  10189  coftr  10193  inaprc  10757  nosepon  27654  fissorduni  35278  r1filimi  35291  satfn  35590  rdgprc  36027  limsucncmpi  36680  limexissup  43733  limexissupab  43735  nadd2rabord  43837  nadd1rabord  43841