smocdmdom

Description: The codomain of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013)

		Ref	Expression
	Assertion	smocdmdom	$⊢ (F : A ⟶ B \land Smo F \land Ord B) \to A \subseteq B$

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to F : A ⟶ B$
2	1	ffnd	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to F Fn A$
3		simpl2	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to Smo F$
4		smodm2	$⊢ (F Fn A \land Smo F) \to Ord A$
5	2 3 4	syl2anc	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to Ord A$
6		ordelord	$⊢ (Ord A \land x \in A) \to Ord x$
7	5 6	sylancom	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to Ord x$
8		simpl3	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to Ord B$
9		simpr	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to x \in A$
10		smogt	$⊢ (F Fn A \land Smo F \land x \in A) \to x \subseteq F (x)$
11	2 3 9 10	syl3anc	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to x \subseteq F (x)$
12		ffvelcdm	$⊢ (F : A ⟶ B \land x \in A) \to F (x) \in B$
13	12	3ad2antl1	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to F (x) \in B$
14		ordtr2	$⊢ (Ord x \land Ord B) \to ((x \subseteq F (x) \land F (x) \in B) \to x \in B)$
15	14	imp	$⊢ ((Ord x \land Ord B) \land (x \subseteq F (x) \land F (x) \in B)) \to x \in B$
16	7 8 11 13 15	syl22anc	$⊢ ((F : A ⟶ B \land Smo F \land Ord B) \land x \in A) \to x \in B$
17	16	ex	$⊢ (F : A ⟶ B \land Smo F \land Ord B) \to (x \in A \to x \in B)$
18	17	ssrdv	$⊢ (F : A ⟶ B \land Smo F \land Ord B) \to A \subseteq B$

Metamath Proof Explorer