Theorem ordsson 7783

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 7777	. 2 ⊢ Ord On
2		ordeleqon 7782	. . . 4 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	birani 508	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
4		ordsseleq 6392	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
5	3, 4	mpbird 260	. 2 ⊢ ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
6	1, 5	mpan2 703	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ⊆ wss 3906  Ord word 6361  Oncon0 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6365  df-on 6366

This theorem is referenced by:  dford5  7784  onss  7785  orduni  7789  ordsuci  7808  ordsucuniel  7821  ordsucuni  7826  iordsmo  8345  dfrecs3  8360  tfr2b  8384  tz7.44-2  8395  ordiso2  9478  ordtypelem7  9487  ordtypelem8  9488  oiid  9504  r1tr  9749  r1ordg  9751  r1ord3g  9752  r1pwss  9757  r1val1  9759  rankwflemb  9766  r1elwf  9769  rankr1ai  9771  cflim2  10248  cfss  10250  cfslb  10251  cfslbn  10252  cfslb2n  10253  cofsmo  10254  coftr  10258  inaprc  10822  nosepon  27810  fissorduni  35461  r1filimi  35478  satfn  35828  rdgprc  36265  limsucncmpi  36937  limexissup  43991  limexissupab  43993  nadd2rabord  44095  nadd1rabord  44099