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 ( 𝐴 , 𝐵 ) ) )