Theorem ordsson 7791

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 7785	. 2 ⊢ Ord On
2		ordeleqon 7790	. . . 4 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	birani 509	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
4		ordsseleq 6397	. . 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 2146   ⊆ wss 3908  Ord word 6366  Oncon0 6367

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371

This theorem is used by:  dford5  7792  onss  7793  orduni  7797  ordsuci  7816  ordsucuniel  7829  ordsucuni  7834  iordsmo  8353  dfrecs3  8368  tfr2b  8392  tz7.44-2  8403  ordiso2  9487  ordtypelem7  9496  ordtypelem8  9497  oiid  9513  r1tr  9758  r1ordg  9760  r1ord3g  9761  r1pwss  9766  r1val1  9768  rankwflemb  9775  r1elwf  9778  rankr1ai  9780  cflim2  10265  cfss  10267  cfslb  10268  cfslbn  10269  cfslb2n  10270  cofsmo  10271  coftr  10275  inaprc  10839  nosepon  27866  fissorduni  35505  r1filimi  35522  satfn  35868  rdgprc  36305  limsucncmpi  36997  limexissup  44049  limexissupab  44051  nadd2rabord  44153  nadd1rabord  44157