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 𝐹 ∧ 𝐺 = 𝐹 ) ) )