Metamath Proof Explorer

Theorem ordiso

Description: Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009) (Proof shortened by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion ordiso ⊢ A ∈ On ∧ B ∈ On → A = B ↔ ∃ f f Isom E , E A B

Proof

Step Hyp Ref Expression
1 resiexg ⊢ A ∈ On → I ↾ A ∈ V
2 isoid ⊢ I ↾ A Isom E , E A A
3 isoeq1 ⊢ f = I ↾ A → f Isom E , E A A ↔ I ↾ A Isom E , E A A
4 3 spcegv ⊢ I ↾ A ∈ V → I ↾ A Isom E , E A A → ∃ f f Isom E , E A A
5 1 2 4 mpisyl ⊢ A ∈ On → ∃ f f Isom E , E A A
6 5 adantr ⊢ A ∈ On ∧ B ∈ On → ∃ f f Isom E , E A A
7 isoeq5 ⊢ A = B → f Isom E , E A A ↔ f Isom E , E A B
8 7 exbidv ⊢ A = B → ∃ f f Isom E , E A A ↔ ∃ f f Isom E , E A B
9 6 8 syl5ibcom ⊢ A ∈ On ∧ B ∈ On → A = B → ∃ f f Isom E , E A B
10 eloni ⊢ A ∈ On → Ord ⁡ A
11 eloni ⊢ B ∈ On → Ord ⁡ B
12 ordiso2 ⊢ f Isom E , E A B ∧ Ord ⁡ A ∧ Ord ⁡ B → A = B
13 12 3coml ⊢ Ord ⁡ A ∧ Ord ⁡ B ∧ f Isom E , E A B → A = B
14 13 3expia ⊢ Ord ⁡ A ∧ Ord ⁡ B → f Isom E , E A B → A = B
15 10 11 14 syl2an ⊢ A ∈ On ∧ B ∈ On → f Isom E , E A B → A = B
16 15 exlimdv ⊢ A ∈ On ∧ B ∈ On → ∃ f f Isom E , E A B → A = B
17 9 16 impbid ⊢ A ∈ On ∧ B ∈ On → A = B ↔ ∃ f f Isom E , E A B