Theorem ordsson 7762

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 7756	. 2 ⊢ Ord On
2		ordeleqon 7761	. . . 4 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	birani 507	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
4		ordsseleq 6371	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
5	3, 4	mpbird 259	. 2 ⊢ ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
6	1, 5	mpan2 701	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858   = wceq 1559   ∈ wcel 2141   ⊆ wss 3904  Ord word 6341  Oncon0 6342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346

This theorem is referenced by:  dford5  7763  onss  7764  orduni  7768  ordsuci  7787  ordsucuniel  7800  ordsucuni  7805  iordsmo  8323  dfrecs3  8338  tfr2b  8362  tz7.44-2  8373  ordiso2  9460  ordtypelem7  9469  ordtypelem8  9470  oiid  9486  r1tr  9731  r1ordg  9733  r1ord3g  9734  r1pwss  9739  r1val1  9741  rankwflemb  9748  r1elwf  9751  rankr1ai  9753  cflim2  10217  cfss  10219  cfslb  10220  cfslbn  10221  cfslb2n  10222  cofsmo  10223  coftr  10227  inaprc  10791  nosepon  27706  fissorduni  35349  r1filimi  35363  satfn  35669  rdgprc  36106  limsucncmpi  36769  limexissup  43822  limexissupab  43824  nadd2rabord  43926  nadd1rabord  43930