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

Metamath Proof Explorer

Theorem ordelon

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

Ref Expression
Assertion ordelon ⊢ Ord ⁡ A ∧ B ∈ A → B ∈ On

Proof

Step Hyp Ref Expression
1 ordelord ⊢ Ord ⁡ A ∧ B ∈ A → Ord ⁡ B
2 elong ⊢ B ∈ A → B ∈ On ↔ Ord ⁡ B
3 2 adantl ⊢ Ord ⁡ A ∧ B ∈ A → B ∈ On ↔ Ord ⁡ B
4 1 3 mpbird ⊢ Ord ⁡ A ∧ B ∈ A → B ∈ On