Step |
Hyp |
Ref |
Expression |
1 |
|
oicl.1 |
|- F = OrdIso ( R , A ) |
2 |
1
|
ordtype |
|- ( ( R We A /\ R Se A ) -> F Isom _E , R ( dom F , A ) ) |
3 |
|
isof1o |
|- ( F Isom _E , R ( dom F , A ) -> F : dom F -1-1-onto-> A ) |
4 |
|
f1of1 |
|- ( F : dom F -1-1-onto-> A -> F : dom F -1-1-> A ) |
5 |
2 3 4
|
3syl |
|- ( ( R We A /\ R Se A ) -> F : dom F -1-1-> A ) |
6 |
|
f1f |
|- ( F : dom F -1-1-> A -> F : dom F --> A ) |
7 |
|
f1dmex |
|- ( ( F : dom F -1-1-> A /\ A e. V ) -> dom F e. _V ) |
8 |
|
fex |
|- ( ( F : dom F --> A /\ dom F e. _V ) -> F e. _V ) |
9 |
6 7 8
|
syl2an2r |
|- ( ( F : dom F -1-1-> A /\ A e. V ) -> F e. _V ) |
10 |
9
|
expcom |
|- ( A e. V -> ( F : dom F -1-1-> A -> F e. _V ) ) |
11 |
5 10
|
syl5 |
|- ( A e. V -> ( ( R We A /\ R Se A ) -> F e. _V ) ) |
12 |
1
|
oi0 |
|- ( -. ( R We A /\ R Se A ) -> F = (/) ) |
13 |
|
0ex |
|- (/) e. _V |
14 |
12 13
|
eqeltrdi |
|- ( -. ( R We A /\ R Se A ) -> F e. _V ) |
15 |
11 14
|
pm2.61d1 |
|- ( A e. V -> F e. _V ) |