Metamath Proof Explorer


Theorem oieu

Description: Uniqueness of the unique ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1
|- F = OrdIso ( R , A )
Assertion oieu
|- ( ( R We A /\ R Se A ) -> ( ( Ord B /\ G Isom _E , R ( B , A ) ) <-> ( B = dom F /\ G = F ) ) )

Proof

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