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 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion oieu ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → ( ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ↔ ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 oicl.1 𝐹 = OrdIso ( 𝑅 , 𝐴 )
2 simprr ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → 𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) )
3 1 ordtype ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
4 3 adantr ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
5 isocnv ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) → 𝐹 Isom 𝑅 , E ( 𝐴 , dom 𝐹 ) )
6 4 5 syl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → 𝐹 Isom 𝑅 , E ( 𝐴 , dom 𝐹 ) )
7 isotr ( ( 𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ∧ 𝐹 Isom 𝑅 , E ( 𝐴 , dom 𝐹 ) ) → ( 𝐹𝐺 ) Isom E , E ( 𝐵 , dom 𝐹 ) )
8 2 6 7 syl2anc ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → ( 𝐹𝐺 ) Isom E , E ( 𝐵 , dom 𝐹 ) )
9 simprl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → Ord 𝐵 )
10 1 oicl Ord dom 𝐹
11 10 a1i ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → Ord dom 𝐹 )
12 ordiso2 ( ( ( 𝐹𝐺 ) Isom E , E ( 𝐵 , dom 𝐹 ) ∧ Ord 𝐵 ∧ Ord dom 𝐹 ) → 𝐵 = dom 𝐹 )
13 8 9 11 12 syl3anc ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → 𝐵 = dom 𝐹 )
14 ordwe ( Ord 𝐵 → E We 𝐵 )
15 14 ad2antrl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → E We 𝐵 )
16 epse E Se 𝐵
17 16 a1i ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → E Se 𝐵 )
18 isoeq4 ( 𝐵 = dom 𝐹 → ( 𝐹 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ↔ 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ) )
19 13 18 syl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → ( 𝐹 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ↔ 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ) )
20 4 19 mpbird ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → 𝐹 Isom E , 𝑅 ( 𝐵 , 𝐴 ) )
21 weisoeq ( ( ( E We 𝐵 ∧ E Se 𝐵 ) ∧ ( 𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ∧ 𝐹 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → 𝐺 = 𝐹 )
22 15 17 2 20 21 syl22anc ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → 𝐺 = 𝐹 )
23 13 22 jca ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) → ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) )
24 23 ex ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → ( ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) → ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) ) )
25 3 10 jctil ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → ( Ord dom 𝐹𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ) )
26 ordeq ( 𝐵 = dom 𝐹 → ( Ord 𝐵 ↔ Ord dom 𝐹 ) )
27 26 adantr ( ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) → ( Ord 𝐵 ↔ Ord dom 𝐹 ) )
28 isoeq4 ( 𝐵 = dom 𝐹 → ( 𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ↔ 𝐺 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ) )
29 isoeq1 ( 𝐺 = 𝐹 → ( 𝐺 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ↔ 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ) )
30 28 29 sylan9bb ( ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) → ( 𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ↔ 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ) )
31 27 30 anbi12d ( ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) → ( ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ↔ ( Ord dom 𝐹𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ) ) )
32 25 31 syl5ibrcom ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → ( ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) → ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ) )
33 24 32 impbid ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → ( ( Ord 𝐵𝐺 Isom E , 𝑅 ( 𝐵 , 𝐴 ) ) ↔ ( 𝐵 = dom 𝐹𝐺 = 𝐹 ) ) )