Theorem ordelon 6389

Description: An element of an ordinal class is an ordinal number. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)

Assertion

Ref	Expression
ordelon	⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Proof of Theorem ordelon

Step	Hyp	Ref	Expression
1		ordelord 6387	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
2		elong 6373	. . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐵 ∈ On ↔ Ord 𝐵))
3	2	adantl 487	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ∈ On ↔ Ord 𝐵))
4	1, 3	mpbird 260	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  Ord word 6364  Oncon0 6365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369

This theorem is used by:  onelon  6390  ordunidif  6416  ordpwsuc  7830  ordsucun  7840  ordunel  7842  ordunisuc2  7859  oesuclem  8540  odi  8594  oelim2  8611  oeoalem  8612  oeoelem  8614  limenpsi  9178  ordtypelem9  9527  oismo  9541  cantnflt  9680  cantnfp1lem3  9688  cantnflem1b  9694  cantnflem1  9697  rankr1bg  9818  rankr1clem  9836  rankr1c  9837  rankonidlem  9845  infxpenlem  10099  coflim  10346  fin23lem26  10410  fpwwe2lem7  10729  onsuct0  37325  ordnexbtwnsuc  44378  orddif0suc  44379  omord2lim  44411  nadd2rabtr  44495  nadd2rabex  44497  nadd1rabtr  44499  nadd1rabex  44501  iunord  50967