Theorem ordsson 7772

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 7766	. 2 ⊢ Ord On
2		ordeleqon 7771	. . . . 5 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	biimpi 215	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ On ∨ 𝐴 = On))
4	3	adantr 479	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
5		ordsseleq 6392	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
6	4, 5	mpbird 256	. 2 ⊢ ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
7	1, 6	mpan2 687	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

Syntax hints:   → wi 4   ∧ wa 394   ∨ wo 843   = wceq 1539   ∈ wcel 2104   ⊆ wss 3947  Ord word 6362  Oncon0 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6366  df-on 6367

This theorem is referenced by:  dford5  7773  onss  7774  orduni  7779  ordsuci  7798  ordsucuniel  7814  ordsucuni  7819  iordsmo  8359  dfrecs3  8374  dfrecs3OLD  8375  tfr2b  8398  tz7.44-2  8409  ordiso2  9512  ordtypelem7  9521  ordtypelem8  9522  oiid  9538  r1tr  9773  r1ordg  9775  r1ord3g  9776  r1pwss  9781  r1val1  9783  rankwflemb  9790  r1elwf  9793  rankr1ai  9795  cflim2  10260  cfss  10262  cfslb  10263  cfslbn  10264  cfslb2n  10265  cofsmo  10266  coftr  10270  inaprc  10833  nosepon  27404  satfn  34644  rdgprc  35070  limsucncmpi  35633  limexissup  42333  limexissupab  42335  nadd2rabord  42437  nadd1rabord  42441