Step |
Hyp |
Ref |
Expression |
1 |
|
isof1o |
|- ( F Isom _E , _E ( A , B ) -> F : A -1-1-onto-> B ) |
2 |
|
f1of |
|- ( F : A -1-1-onto-> B -> F : A --> B ) |
3 |
1 2
|
syl |
|- ( F Isom _E , _E ( A , B ) -> F : A --> B ) |
4 |
|
ffdm |
|- ( F : A --> B -> ( F : dom F --> B /\ dom F C_ A ) ) |
5 |
4
|
simpld |
|- ( F : A --> B -> F : dom F --> B ) |
6 |
|
fss |
|- ( ( F : dom F --> B /\ B C_ On ) -> F : dom F --> On ) |
7 |
5 6
|
sylan |
|- ( ( F : A --> B /\ B C_ On ) -> F : dom F --> On ) |
8 |
7
|
3adant2 |
|- ( ( F : A --> B /\ Ord A /\ B C_ On ) -> F : dom F --> On ) |
9 |
3 8
|
syl3an1 |
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> F : dom F --> On ) |
10 |
|
fdm |
|- ( F : A --> B -> dom F = A ) |
11 |
10
|
eqcomd |
|- ( F : A --> B -> A = dom F ) |
12 |
|
ordeq |
|- ( A = dom F -> ( Ord A <-> Ord dom F ) ) |
13 |
1 2 11 12
|
4syl |
|- ( F Isom _E , _E ( A , B ) -> ( Ord A <-> Ord dom F ) ) |
14 |
13
|
biimpa |
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A ) -> Ord dom F ) |
15 |
14
|
3adant3 |
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Ord dom F ) |
16 |
10
|
eleq2d |
|- ( F : A --> B -> ( x e. dom F <-> x e. A ) ) |
17 |
10
|
eleq2d |
|- ( F : A --> B -> ( y e. dom F <-> y e. A ) ) |
18 |
16 17
|
anbi12d |
|- ( F : A --> B -> ( ( x e. dom F /\ y e. dom F ) <-> ( x e. A /\ y e. A ) ) ) |
19 |
1 2 18
|
3syl |
|- ( F Isom _E , _E ( A , B ) -> ( ( x e. dom F /\ y e. dom F ) <-> ( x e. A /\ y e. A ) ) ) |
20 |
|
isorel |
|- ( ( F Isom _E , _E ( A , B ) /\ ( x e. A /\ y e. A ) ) -> ( x _E y <-> ( F ` x ) _E ( F ` y ) ) ) |
21 |
|
epel |
|- ( x _E y <-> x e. y ) |
22 |
|
fvex |
|- ( F ` y ) e. _V |
23 |
22
|
epeli |
|- ( ( F ` x ) _E ( F ` y ) <-> ( F ` x ) e. ( F ` y ) ) |
24 |
20 21 23
|
3bitr3g |
|- ( ( F Isom _E , _E ( A , B ) /\ ( x e. A /\ y e. A ) ) -> ( x e. y <-> ( F ` x ) e. ( F ` y ) ) ) |
25 |
24
|
biimpd |
|- ( ( F Isom _E , _E ( A , B ) /\ ( x e. A /\ y e. A ) ) -> ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) |
26 |
25
|
ex |
|- ( F Isom _E , _E ( A , B ) -> ( ( x e. A /\ y e. A ) -> ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) ) |
27 |
19 26
|
sylbid |
|- ( F Isom _E , _E ( A , B ) -> ( ( x e. dom F /\ y e. dom F ) -> ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) ) |
28 |
27
|
ralrimivv |
|- ( F Isom _E , _E ( A , B ) -> A. x e. dom F A. y e. dom F ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) |
29 |
28
|
3ad2ant1 |
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> A. x e. dom F A. y e. dom F ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) |
30 |
|
df-smo |
|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. dom F ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) ) |
31 |
9 15 29 30
|
syl3anbrc |
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Smo F ) |