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 ffvelrn ( ( 𝐹 : 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 )