Theorem ordelon 6388

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 6386	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
2		elong 6372	. . 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 2146  Ord word 6363  Oncon0 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368

This theorem is used by:  onelon  6389  ordunidif  6415  ordpwsuc  7813  ordsucun  7823  ordunel  7825  ordunisuc2  7842  oesuclem  8512  odi  8566  oelim2  8583  oeoalem  8584  oeoelem  8586  limenpsi  9143  ordtypelem9  9491  oismo  9505  cantnflt  9644  cantnfp1lem3  9652  cantnflem1b  9658  cantnflem1  9661  rankr1bg  9778  rankr1clem  9795  rankr1c  9796  rankonidlem  9803  infxpenlem  10009  coflim  10256  fin23lem26  10320  fpwwe2lem7  10633  onsuct0  36985  ordnexbtwnsuc  44027  orddif0suc  44028  omord2lim  44060  nadd2rabtr  44144  nadd2rabex  44146  nadd1rabtr  44148  nadd1rabex  44150  iunord  50487