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 6385	. . 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 3899  Ord word 6354  Oncon0 6355

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359

This theorem is used by:  dford5  7787  onss  7788  orduni  7792  ordsuci  7811  ordsucuniel  7824  ordsucuni  7829  iordsmo  8349  dfrecs3  8364  tfr2b  8388  tz7.44-2  8399  fissorduni  9266  ordiso2  9493  ordtypelem7  9502  ordtypelem8  9503  oiid  9519  r1tr  9766  r1ordg  9768  r1ord3g  9769  r1pwss  9774  r1val1  9776  rankwflemb  9783  r1elwf  9786  rankr1ai  9788  r1filimi  9884  cflim2  10322  cfss  10324  cfslb  10325  cfslbn  10326  cfslb2n  10327  cofsmo  10328  coftr  10332  inaprc  10902  nosepon  28004  satfn  36089  rdgprc  36526  limsucncmpi  37203  limexissup  44241  limexissupab  44243  nadd2rabord  44345  nadd1rabord  44349