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 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐵 ‘ 𝐴 ) ∈ On )

Proof

Step	Hyp	Ref	Expression
1		df-smo	⊢ ( Smo 𝐵 ↔ ( 𝐵 : dom 𝐵 ⟶ On ∧ Ord dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
2	1	simp1bi	⊢ ( Smo 𝐵 → 𝐵 : dom 𝐵 ⟶ On )
3	2	ffvelrnda	⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐵 ‘ 𝐴 ) ∈ On )