Theorem ordelon 6365

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 6363	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
2		elong 6349	. . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐵 ∈ On ↔ Ord 𝐵))
3	2	adantl 485	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ∈ On ↔ Ord 𝐵))
4	1, 3	mpbird 259	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  Ord word 6340  Oncon0 6341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-tr 5205  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-ord 6344  df-on 6345

This theorem is referenced by:  onelon  6366  ordunidif  6391  ordpwsuc  7790  ordsucun  7800  ordunel  7802  ordunisuc2  7819  oesuclem  8488  odi  8542  oelim2  8559  oeoalem  8560  oeoelem  8562  limenpsi  9118  ordtypelem9  9468  oismo  9482  cantnflt  9621  cantnfp1lem3  9629  cantnflem1b  9635  cantnflem1  9638  rankr1bg  9755  rankr1clem  9772  rankr1c  9773  rankonidlem  9780  infxpenlem  9963  coflim  10212  fin23lem26  10276  fpwwe2lem7  10589  onsuct0  36762  ordnexbtwnsuc  43805  orddif0suc  43806  omord2lim  43838  nadd2rabtr  43922  nadd2rabex  43924  nadd1rabtr  43926  nadd1rabex  43928  iunord  50258