Step |
Hyp |
Ref |
Expression |
1 |
|
dfsmo2 |
|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
2 |
1
|
simp1bi |
|- ( Smo F -> F : dom F --> On ) |
3 |
2
|
ffund |
|- ( Smo F -> Fun F ) |
4 |
|
funres |
|- ( Fun F -> Fun ( F |` A ) ) |
5 |
4
|
funfnd |
|- ( Fun F -> ( F |` A ) Fn dom ( F |` A ) ) |
6 |
3 5
|
syl |
|- ( Smo F -> ( F |` A ) Fn dom ( F |` A ) ) |
7 |
|
df-ima |
|- ( F " A ) = ran ( F |` A ) |
8 |
|
imassrn |
|- ( F " A ) C_ ran F |
9 |
7 8
|
eqsstrri |
|- ran ( F |` A ) C_ ran F |
10 |
2
|
frnd |
|- ( Smo F -> ran F C_ On ) |
11 |
9 10
|
sstrid |
|- ( Smo F -> ran ( F |` A ) C_ On ) |
12 |
|
df-f |
|- ( ( F |` A ) : dom ( F |` A ) --> On <-> ( ( F |` A ) Fn dom ( F |` A ) /\ ran ( F |` A ) C_ On ) ) |
13 |
6 11 12
|
sylanbrc |
|- ( Smo F -> ( F |` A ) : dom ( F |` A ) --> On ) |
14 |
13
|
adantr |
|- ( ( Smo F /\ Ord A ) -> ( F |` A ) : dom ( F |` A ) --> On ) |
15 |
|
smodm |
|- ( Smo F -> Ord dom F ) |
16 |
|
ordin |
|- ( ( Ord A /\ Ord dom F ) -> Ord ( A i^i dom F ) ) |
17 |
|
dmres |
|- dom ( F |` A ) = ( A i^i dom F ) |
18 |
|
ordeq |
|- ( dom ( F |` A ) = ( A i^i dom F ) -> ( Ord dom ( F |` A ) <-> Ord ( A i^i dom F ) ) ) |
19 |
17 18
|
ax-mp |
|- ( Ord dom ( F |` A ) <-> Ord ( A i^i dom F ) ) |
20 |
16 19
|
sylibr |
|- ( ( Ord A /\ Ord dom F ) -> Ord dom ( F |` A ) ) |
21 |
20
|
ancoms |
|- ( ( Ord dom F /\ Ord A ) -> Ord dom ( F |` A ) ) |
22 |
15 21
|
sylan |
|- ( ( Smo F /\ Ord A ) -> Ord dom ( F |` A ) ) |
23 |
|
resss |
|- ( F |` A ) C_ F |
24 |
|
dmss |
|- ( ( F |` A ) C_ F -> dom ( F |` A ) C_ dom F ) |
25 |
23 24
|
ax-mp |
|- dom ( F |` A ) C_ dom F |
26 |
1
|
simp3bi |
|- ( Smo F -> A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) |
27 |
|
ssralv |
|- ( dom ( F |` A ) C_ dom F -> ( A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) -> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
28 |
25 26 27
|
mpsyl |
|- ( Smo F -> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) ) |
29 |
28
|
adantr |
|- ( ( Smo F /\ Ord A ) -> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) ) |
30 |
|
ordtr1 |
|- ( Ord dom ( F |` A ) -> ( ( y e. x /\ x e. dom ( F |` A ) ) -> y e. dom ( F |` A ) ) ) |
31 |
22 30
|
syl |
|- ( ( Smo F /\ Ord A ) -> ( ( y e. x /\ x e. dom ( F |` A ) ) -> y e. dom ( F |` A ) ) ) |
32 |
|
inss1 |
|- ( A i^i dom F ) C_ A |
33 |
17 32
|
eqsstri |
|- dom ( F |` A ) C_ A |
34 |
33
|
sseli |
|- ( y e. dom ( F |` A ) -> y e. A ) |
35 |
31 34
|
syl6 |
|- ( ( Smo F /\ Ord A ) -> ( ( y e. x /\ x e. dom ( F |` A ) ) -> y e. A ) ) |
36 |
35
|
expcomd |
|- ( ( Smo F /\ Ord A ) -> ( x e. dom ( F |` A ) -> ( y e. x -> y e. A ) ) ) |
37 |
36
|
imp31 |
|- ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> y e. A ) |
38 |
37
|
fvresd |
|- ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> ( ( F |` A ) ` y ) = ( F ` y ) ) |
39 |
33
|
sseli |
|- ( x e. dom ( F |` A ) -> x e. A ) |
40 |
39
|
fvresd |
|- ( x e. dom ( F |` A ) -> ( ( F |` A ) ` x ) = ( F ` x ) ) |
41 |
40
|
ad2antlr |
|- ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> ( ( F |` A ) ` x ) = ( F ` x ) ) |
42 |
38 41
|
eleq12d |
|- ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> ( ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) <-> ( F ` y ) e. ( F ` x ) ) ) |
43 |
42
|
ralbidva |
|- ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) -> ( A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) <-> A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
44 |
43
|
ralbidva |
|- ( ( Smo F /\ Ord A ) -> ( A. x e. dom ( F |` A ) A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) <-> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
45 |
29 44
|
mpbird |
|- ( ( Smo F /\ Ord A ) -> A. x e. dom ( F |` A ) A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) ) |
46 |
|
dfsmo2 |
|- ( Smo ( F |` A ) <-> ( ( F |` A ) : dom ( F |` A ) --> On /\ Ord dom ( F |` A ) /\ A. x e. dom ( F |` A ) A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) ) ) |
47 |
14 22 45 46
|
syl3anbrc |
|- ( ( Smo F /\ Ord A ) -> Smo ( F |` A ) ) |