issmo2

Description: Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013)

		Ref	Expression
	Assertion	issmo2	$⊢ F : A ⟶ B \to ((B \subseteq On \land Ord A \land \forall x \in A \forall y \in x F (y) \in F (x)) \to Smo F)$

Step	Hyp	Ref	Expression
1		fss	$⊢ (F : A ⟶ B \land B \subseteq On) \to F : A ⟶ On$
2	1	ex	$⊢ F : A ⟶ B \to (B \subseteq On \to F : A ⟶ On)$
3		fdm	$⊢ F : A ⟶ B \to dom F = A$
4	3	feq2d	$⊢ F : A ⟶ B \to (F : dom F ⟶ On \leftrightarrow F : A ⟶ On)$
5	2 4	sylibrd	$⊢ F : A ⟶ B \to (B \subseteq On \to F : dom F ⟶ On)$
6		ordeq	$⊢ dom F = A \to (Ord dom F \leftrightarrow Ord A)$
7	3 6	syl	$⊢ F : A ⟶ B \to (Ord dom F \leftrightarrow Ord A)$
8	7	biimprd	$⊢ F : A ⟶ B \to (Ord A \to Ord dom F)$
9	3	raleqdv	$⊢ F : A ⟶ B \to (\forall x \in dom F \forall y \in x F (y) \in F (x) \leftrightarrow \forall x \in A \forall y \in x F (y) \in F (x))$
10	9	biimprd	$⊢ F : A ⟶ B \to (\forall x \in A \forall y \in x F (y) \in F (x) \to \forall x \in dom F \forall y \in x F (y) \in F (x))$
11	5 8 10	3anim123d	$⊢ F : A ⟶ B \to ((B \subseteq On \land Ord A \land \forall x \in A \forall y \in x F (y) \in F (x)) \to (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x)))$
12		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))$
13	11 12	syl6ibr	$⊢ F : A ⟶ B \to ((B \subseteq On \land Ord A \land \forall x \in A \forall y \in x F (y) \in F (x)) \to Smo F)$

Metamath Proof Explorer