Theorem smofvon2

Description: The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013)

	Ref	Expression
Assertion	smofvon2	⊢ ( Smo 𝐹 → ( 𝐹 ‘ 𝐵 ) ∈ On )

Proof

Step	Hyp	Ref	Expression
1		dfsmo2	⊢ ( Smo 𝐹 ↔ ( 𝐹 : dom 𝐹 ⟶ On ∧ Ord dom 𝐹 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
2	1	simp1bi	⊢ ( Smo 𝐹 → 𝐹 : dom 𝐹 ⟶ On )
3		ffvelcdm	⊢ ( ( 𝐹 : dom 𝐹 ⟶ On ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐵 ) ∈ On )
4	3	expcom	⊢ ( 𝐵 ∈ dom 𝐹 → ( 𝐹 : dom 𝐹 ⟶ On → ( 𝐹 ‘ 𝐵 ) ∈ On ) )
5	2 4	syl5	⊢ ( 𝐵 ∈ dom 𝐹 → ( Smo 𝐹 → ( 𝐹 ‘ 𝐵 ) ∈ On ) )
6		ndmfv	⊢ ( ¬ 𝐵 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐵 ) = ∅ )
7		0elon	⊢ ∅ ∈ On
8	6 7	eqeltrdi	⊢ ( ¬ 𝐵 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐵 ) ∈ On )
9	8	a1d	⊢ ( ¬ 𝐵 ∈ dom 𝐹 → ( Smo 𝐹 → ( 𝐹 ‘ 𝐵 ) ∈ On ) )
10	5 9	pm2.61i	⊢ ( Smo 𝐹 → ( 𝐹 ‘ 𝐵 ) ∈ On )