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	⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → Ord 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		smodm	⊢ ( Smo 𝐹 → Ord dom 𝐹 )
2		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
3		ordeq	⊢ ( dom 𝐹 = 𝐴 → ( Ord dom 𝐹 ↔ Ord 𝐴 ) )
4	2 3	syl	⊢ ( 𝐹 Fn 𝐴 → ( Ord dom 𝐹 ↔ Ord 𝐴 ) )
5	4	biimpa	⊢ ( ( 𝐹 Fn 𝐴 ∧ Ord dom 𝐹 ) → Ord 𝐴 )
6	1 5	sylan2	⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → Ord 𝐴 )