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

Metamath Proof Explorer

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 )