Metamath Proof Explorer


Theorem smorndom

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

Ref Expression
Assertion smorndom
|- ( ( F : A --> B /\ Smo F /\ Ord B ) -> A C_ B )

Proof

Step Hyp Ref Expression
1 simpl1
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> F : A --> B )
2 1 ffnd
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> F Fn A )
3 simpl2
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> Smo F )
4 smodm2
 |-  ( ( F Fn A /\ Smo F ) -> Ord A )
5 2 3 4 syl2anc
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> Ord A )
6 ordelord
 |-  ( ( Ord A /\ x e. A ) -> Ord x )
7 5 6 sylancom
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> Ord x )
8 simpl3
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> Ord B )
9 simpr
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> x e. A )
10 smogt
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> x C_ ( F ` x ) )
11 2 3 9 10 syl3anc
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> x C_ ( F ` x ) )
12 ffvelrn
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
13 12 3ad2antl1
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> ( F ` x ) e. B )
14 ordtr2
 |-  ( ( Ord x /\ Ord B ) -> ( ( x C_ ( F ` x ) /\ ( F ` x ) e. B ) -> x e. B ) )
15 14 imp
 |-  ( ( ( Ord x /\ Ord B ) /\ ( x C_ ( F ` x ) /\ ( F ` x ) e. B ) ) -> x e. B )
16 7 8 11 13 15 syl22anc
 |-  ( ( ( F : A --> B /\ Smo F /\ Ord B ) /\ x e. A ) -> x e. B )
17 16 ex
 |-  ( ( F : A --> B /\ Smo F /\ Ord B ) -> ( x e. A -> x e. B ) )
18 17 ssrdv
 |-  ( ( F : A --> B /\ Smo F /\ Ord B ) -> A C_ B )