Metamath Proof Explorer

Theorem 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 /\ 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 ffvelcdm 
 |-  ( ( 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 )