Theorem ordsson 7801

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 7795	. 2 ⊢ Ord On
2		ordeleqon 7800	. . . . 5 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	biimpi 216	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ On ∨ 𝐴 = On))
4	3	adantr 480	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
5		ordsseleq 6414	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
6	4, 5	mpbird 257	. 2 ⊢ ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
7	1, 6	mpan2 691	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1536   ∈ wcel 2105   ⊆ wss 3962  Ord word 6384  Oncon0 6385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389

This theorem is referenced by:  dford5  7802  onss  7803  orduni  7808  ordsuci  7827  ordsucuniel  7843  ordsucuni  7848  iordsmo  8395  dfrecs3  8410  dfrecs3OLD  8411  tfr2b  8434  tz7.44-2  8445  ordiso2  9552  ordtypelem7  9561  ordtypelem8  9562  oiid  9578  r1tr  9813  r1ordg  9815  r1ord3g  9816  r1pwss  9821  r1val1  9823  rankwflemb  9830  r1elwf  9833  rankr1ai  9835  cflim2  10300  cfss  10302  cfslb  10303  cfslbn  10304  cfslb2n  10305  cofsmo  10306  coftr  10310  inaprc  10873  nosepon  27724  satfn  35339  rdgprc  35775  limsucncmpi  36427  limexissup  43270  limexissupab  43272  nadd2rabord  43374  nadd1rabord  43378