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