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 -1 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 -1 Isom R , E A dom F
7 isotr G Isom E , R B A F -1 Isom R , E A dom F F -1 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 -1 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 -1 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