This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onelon

Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of BellMachover p. 469. Lemma 1.3 of Schloeder p. 1. (Contributed by NM, 26-Oct-2003)

Ref Expression
Assertion onelon ⊢ A ∈ On ∧ B ∈ A → B ∈ On

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 ordelon ⊢ Ord ⁡ A ∧ B ∈ A → B ∈ On
3 1 2 sylan ⊢ A ∈ On ∧ B ∈ A → B ∈ On