Theorem ordsson 7797

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 7791	. 2 ⊢ Ord On
2		ordeleqon 7796	. . . 4 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	birani 509	. . 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 704	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  Ord word 6361  Oncon0 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366

This theorem is used by:  dford5  7798  onss  7799  orduni  7803  ordsuci  7822  ordsucuniel  7835  ordsucuni  7840  iordsmo  8368  dfrecs3  8383  tfr2b  8407  tz7.44-2  8418  fissorduni  9285  ordiso2  9512  ordtypelem7  9521  ordtypelem8  9522  oiid  9538  rnr1  9777  r1tr  9786  r1ordg  9788  r1ord3g  9789  r1pwss  9794  r1val1  9796  rankwflembOLD  9804  r1elwf  9807  rankr1ai  9809  r1filimi  9906  cflim2  10344  cfss  10346  cfslb  10347  cfslbn  10348  cfslb2n  10349  cofsmo  10350  coftr  10354  inaprc  10924  nosepon  28027  satfn  36206  rdgprc  36648  limsucncmpi  37325  limexissup  44376  limexissupab  44378  nadd2rabord  44480  nadd1rabord  44484