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 ) |