Metamath Proof Explorer

Theorem smofvon

Description: If B is a strictly monotone ordinal function, and A is in the domain of B , then the value of the function at A is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011)

		Ref	Expression
	Assertion	smofvon	$⊢ (Smo B \land A \in dom B) \to B (A) \in On$

Proof

Step	Hyp	Ref	Expression
1		df-smo	$⊢ Smo B \leftrightarrow (B : dom B ⟶ On \land Ord dom B \land \forall x \in dom B \forall y \in dom B (x \in y \to B (x) \in B (y)))$
2	1	simp1bi	$⊢ Smo B \to B : dom B ⟶ On$
3	2	ffvelrnda	$⊢ (Smo B \land A \in dom B) \to B (A) \in On$