This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 = 𝐵 ↔ ∃ 𝑓 𝑓 Isom E , E ( 𝐴 , 𝐵 ) ) )

Proof

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