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