Step |
Hyp |
Ref |
Expression |
1 |
|
oicl.1 |
|- F = OrdIso ( R , A ) |
2 |
|
simprr |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> G Isom _E , R ( B , A ) ) |
3 |
1
|
ordtype |
|- ( ( R We A /\ R Se A ) -> F Isom _E , R ( dom F , A ) ) |
4 |
3
|
adantr |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> F Isom _E , R ( dom F , A ) ) |
5 |
|
isocnv |
|- ( F Isom _E , R ( dom F , A ) -> `' F Isom R , _E ( A , dom F ) ) |
6 |
4 5
|
syl |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> `' F Isom R , _E ( A , dom F ) ) |
7 |
|
isotr |
|- ( ( G Isom _E , R ( B , A ) /\ `' F Isom R , _E ( A , dom F ) ) -> ( `' F o. G ) Isom _E , _E ( B , dom F ) ) |
8 |
2 6 7
|
syl2anc |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> ( `' F o. G ) Isom _E , _E ( B , dom F ) ) |
9 |
|
simprl |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> Ord B ) |
10 |
1
|
oicl |
|- Ord dom F |
11 |
10
|
a1i |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> Ord dom F ) |
12 |
|
ordiso2 |
|- ( ( ( `' F o. G ) Isom _E , _E ( B , dom F ) /\ Ord B /\ Ord dom F ) -> B = dom F ) |
13 |
8 9 11 12
|
syl3anc |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> B = dom F ) |
14 |
|
ordwe |
|- ( Ord B -> _E We B ) |
15 |
14
|
ad2antrl |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> _E We B ) |
16 |
|
epse |
|- _E Se B |
17 |
16
|
a1i |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> _E Se B ) |
18 |
|
isoeq4 |
|- ( B = dom F -> ( F Isom _E , R ( B , A ) <-> F Isom _E , R ( dom F , A ) ) ) |
19 |
13 18
|
syl |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> ( F Isom _E , R ( B , A ) <-> F Isom _E , R ( dom F , A ) ) ) |
20 |
4 19
|
mpbird |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> F Isom _E , R ( B , A ) ) |
21 |
|
weisoeq |
|- ( ( ( _E We B /\ _E Se B ) /\ ( G Isom _E , R ( B , A ) /\ F Isom _E , R ( B , A ) ) ) -> G = F ) |
22 |
15 17 2 20 21
|
syl22anc |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> G = F ) |
23 |
13 22
|
jca |
|- ( ( ( R We A /\ R Se A ) /\ ( Ord B /\ G Isom _E , R ( B , A ) ) ) -> ( B = dom F /\ G = F ) ) |
24 |
23
|
ex |
|- ( ( R We A /\ R Se A ) -> ( ( Ord B /\ G Isom _E , R ( B , A ) ) -> ( B = dom F /\ G = F ) ) ) |
25 |
3 10
|
jctil |
|- ( ( R We A /\ R Se A ) -> ( Ord dom F /\ F Isom _E , R ( dom F , A ) ) ) |
26 |
|
ordeq |
|- ( B = dom F -> ( Ord B <-> Ord dom F ) ) |
27 |
26
|
adantr |
|- ( ( B = dom F /\ G = F ) -> ( Ord B <-> Ord dom F ) ) |
28 |
|
isoeq4 |
|- ( B = dom F -> ( G Isom _E , R ( B , A ) <-> G Isom _E , R ( dom F , A ) ) ) |
29 |
|
isoeq1 |
|- ( G = F -> ( G Isom _E , R ( dom F , A ) <-> F Isom _E , R ( dom F , A ) ) ) |
30 |
28 29
|
sylan9bb |
|- ( ( B = dom F /\ G = F ) -> ( G Isom _E , R ( B , A ) <-> F Isom _E , R ( dom F , A ) ) ) |
31 |
27 30
|
anbi12d |
|- ( ( B = dom F /\ G = F ) -> ( ( Ord B /\ G Isom _E , R ( B , A ) ) <-> ( Ord dom F /\ F Isom _E , R ( dom F , A ) ) ) ) |
32 |
25 31
|
syl5ibrcom |
|- ( ( R We A /\ R Se A ) -> ( ( B = dom F /\ G = F ) -> ( Ord B /\ G Isom _E , R ( B , A ) ) ) ) |
33 |
24 32
|
impbid |
|- ( ( R We A /\ R Se A ) -> ( ( Ord B /\ G Isom _E , R ( B , A ) ) <-> ( B = dom F /\ G = F ) ) ) |