Theorem ordsson 7759

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 7753	. 2 ⊢ Ord On
2		ordeleqon 7758	. . . . 5 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	biimpi 216	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ On ∨ 𝐴 = On))
4	3	adantr 480	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
5		ordsseleq 6361	. . 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 1540   ∈ wcel 2109   ⊆ wss 3914  Ord word 6331  Oncon0 6332

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  dford5  7760  onss  7761  orduni  7765  ordsuci  7784  ordsucuniel  7799  ordsucuni  7804  iordsmo  8326  dfrecs3  8341  tfr2b  8364  tz7.44-2  8375  ordiso2  9468  ordtypelem7  9477  ordtypelem8  9478  oiid  9494  r1tr  9729  r1ordg  9731  r1ord3g  9732  r1pwss  9737  r1val1  9739  rankwflemb  9746  r1elwf  9749  rankr1ai  9751  cflim2  10216  cfss  10218  cfslb  10219  cfslbn  10220  cfslb2n  10221  cofsmo  10222  coftr  10226  inaprc  10789  nosepon  27577  satfn  35342  rdgprc  35782  limsucncmpi  36433  limexissup  43270  limexissupab  43272  nadd2rabord  43374  nadd1rabord  43378