Theorem ordsson 7786

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 7780	. 2 ⊢ Ord On
2		ordeleqon 7785	. . . 4 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	birani 509	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
4		ordsseleq 6391	. . 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 1570   ∈ wcel 2145   ⊆ wss 3902  Ord word 6360  Oncon0 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  dford5  7787  onss  7788  orduni  7792  ordsuci  7811  ordsucuniel  7824  ordsucuni  7829  iordsmo  8350  dfrecs3  8365  tfr2b  8389  tz7.44-2  8400  ordiso2  9491  ordtypelem7  9500  ordtypelem8  9501  oiid  9517  r1tr  9762  r1ordg  9764  r1ord3g  9765  r1pwss  9770  r1val1  9772  rankwflemb  9779  r1elwf  9782  rankr1ai  9784  cflim2  10269  cfss  10271  cfslb  10272  cfslbn  10273  cfslb2n  10274  cofsmo  10275  coftr  10279  inaprc  10849  nosepon  27909  fissorduni  35602  r1filimi  35619  satfn  35942  rdgprc  36379  limsucncmpi  37072  limexissup  44130  limexissupab  44132  nadd2rabord  44234  nadd1rabord  44238