Metamath Proof Explorer

Theorem smodm2

Description: The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013)

Ref Expression
Assertion smodm2 ⊢ F Fn A ∧ Smo ⁡ F → Ord ⁡ A

Proof

Step Hyp Ref Expression
1 smodm ⊢ Smo ⁡ F → Ord ⁡ dom ⁡ F
2 fndm ⊢ F Fn A → dom ⁡ F = A
3 ordeq ⊢ dom ⁡ F = A → Ord ⁡ dom ⁡ F ↔ Ord ⁡ A
4 2 3 syl ⊢ F Fn A → Ord ⁡ dom ⁡ F ↔ Ord ⁡ A
5 4 biimpa ⊢ F Fn A ∧ Ord ⁡ dom ⁡ F → Ord ⁡ A
6 1 5 sylan2 ⊢ F Fn A ∧ Smo ⁡ F → Ord ⁡ A