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 F \to F (B) \in On$

Step	Hyp	Ref	Expression
1		dfsmo2	$⊢ Smo F \leftrightarrow (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x))$
2	1	simp1bi	$⊢ Smo F \to F : dom F ⟶ On$
3		ffvelrn	$⊢ (F : dom F ⟶ On \land B \in dom F) \to F (B) \in On$
4	3	expcom	$⊢ B \in dom F \to (F : dom F ⟶ On \to F (B) \in On)$
5	2 4	syl5	$⊢ B \in dom F \to (Smo F \to F (B) \in On)$
6		ndmfv	$⊢ \neg B \in dom F \to F (B) = \emptyset$
7		0elon	$⊢ \emptyset \in On$
8	6 7	eqeltrdi	$⊢ \neg B \in dom F \to F (B) \in On$
9	8	a1d	$⊢ \neg B \in dom F \to (Smo F \to F (B) \in On)$
10	5 9	pm2.61i	$⊢ Smo F \to F (B) \in On$

Metamath Proof Explorer